Modular Verification of JML Contracts Using Bounded Model Checking

@InProceedings{BeckertKirstenEA20,
  author    = {Bernhard Beckert and
               Michael Kirsten and
               Jonas Klamroth and
               Mattias Ulbrich},
  editor    = {Tiziana Margaria and
               Bernhard Steffen},
  title     = {Modular Verification of {JML} Contracts Using Bounded Model Checking},
  booktitle = {9th International Symposium on Leveraging Applications of Formal Methods,
               Verification and Validation ({ISoLA} 2020)},
  part      = {I: Verification Principles},
  series    = {Lecture Notes in Computer Science},
  pages     = {60--80},
  volume    = {12476},
  publisher = {Springer},
  year      = {2020},
  doi       = {10.1007/978-3-030-61362-4_4},
  month     = oct,
  abstract  = {In this article, we present an overview of recent combinations of
               There are two paradigms for dealing with complex verification targets:
               Modularization using contract-based specifications and whole-program
               analysis. In this paper, we present an approach bridging the gap between
               the two paradigms, introducing concepts from the world of contract-based
               deductive verification into the domain of software bounded model checking.
               \newline

               We present a transformation that takes Java programs annotated with
               contracts written in the Java Modeling Language and turns them into Java
               programs that can be read by the bounded model checker JBMC. A central
               idea of the translation is to make use of nondeterministic value
               assignments to eliminate JML quantifiers. We have implemented our
               approach and discuss an evaluation, which shows the advantages of the
               presented approach.},
  eventdate = {2020-10-26/2020-10-30},
  venue     = {Rhodes, Greece}
}