@inproceedings{35426, author = {{Richter, Cedric and Haltermann, Jan Frederik and Jakobs, Marie-Christine and Pauck, Felix and Schott, Stefan and Wehrheim, Heike}}, booktitle = {{37th IEEE/ACM International Conference on Automated Software Engineering}}, publisher = {{ACM}}, title = {{{Are Neural Bug Detectors Comparable to Software Developers on Variable Misuse Bugs?}}}, doi = {{10.1145/3551349.3561156}}, year = {{2023}}, } @unpublished{17825, abstract = {{Software verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it requires novel implementations for every new technique. In this paper, we employ cooperative verification in order to avoid reimplementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVerCIG allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVerCIG can increase the number of correctly verified tasks without increasing the used resources}}, author = {{Haltermann, Jan Frederik and Wehrheim, Heike}}, booktitle = {{arXiv:2008.04551}}, title = {{{Cooperative Verification via Collective Invariant Generation}}}, year = {{2020}}, } @misc{12885, author = {{Haltermann, Jan Frederik}}, title = {{{Analyzing Data Usage in Array Programs}}}, year = {{2019}}, } @inproceedings{3265, abstract = {{We present CLARC (Cryptographic Library for Anonymous Reputation and Credentials), an anonymous credentials system (ACS) combined with an anonymous reputation system. Using CLARC, users can receive attribute-based credentials from issuers. They can efficiently prove that their credentials satisfy complex (access) policies in a privacy-preserving way. This implements anonymous access control with complex policies. Furthermore, CLARC is the first ACS that is combined with an anonymous reputation system where users can anonymously rate services. A user who gets access to a service via a credential, also anonymously receives a review token to rate the service. If a user creates more than a single rating, this can be detected by anyone, preventing users from spamming ratings to sway public opinion. To evaluate feasibility of our construction, we present an open-source prototype implementation.}}, author = {{Bemmann, Kai and Blömer, Johannes and Bobolz, Jan and Bröcher, Henrik and Diemert, Denis Pascal and Eidens, Fabian and Eilers, Lukas and Haltermann, Jan Frederik and Juhnke, Jakob and Otour, Burhan and Porzenheim, Laurens Alexander and Pukrop, Simon and Schilling, Erik and Schlichtig, Michael and Stienemeier, Marcel}}, booktitle = {{Proceedings of the 13th International Conference on Availability, Reliability and Security - ARES '18}}, isbn = {{978-1-4503-6448-5}}, location = {{Hamburg, Germany}}, publisher = {{ACM}}, title = {{{Fully-Featured Anonymous Credentials with Reputation System}}}, doi = {{10.1145/3230833.3234517}}, year = {{2018}}, } @inproceedings{3414, abstract = {{Over the years, Design by Contract (DbC) has evolved as a powerful concept for program documentation, testing, and verification. Contracts formally specify assertions on (mostly) object-oriented programs: pre- and postconditions of methods, class invariants, allowed call orders, etc. Missing in the long list of properties specifiable by contracts are, however, method correlations: DbC languages fall short on stating assertions relating methods. In this paper, we propose the novel concept of inter-method contract, allowing precisely for expressing method correlations.We present JMC as a language for specifying and JMCTest as a tool for dynamically checking inter-method contracts on Java programs. JMCTest fully automatically generates objects on which the contracted methods are called and the validity of the contract is checked. Using JMCTest, we detected that large Java code bases (e.g. JBoss, Java RT) frequently violate standard inter-method contracts. In comparison to other verification tools inspecting (some) inter-method contracts, JMCTest can find bugs that remain undetected by those tools.}}, author = {{Börding, Paul and Haltermann, Jan Frederik and Jakobs, Marie-Christine and Wehrheim, Heike}}, booktitle = {{Proceedings of the IFIP International Conference on Testing Software and Systems (ICTSS 2018)}}, location = {{Cádiz, Spain}}, pages = {{39----55}}, publisher = {{Springer}}, title = {{{JMCTest: Automatically Testing Inter-Method Contracts in Java}}}, volume = {{11146}}, year = {{2018}}, }