@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}},
}