Modular Verification of JML Contracts Using Bounded Model Checking

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Michael Kirsten, Jonas Klamroth, and Mattias Ulbrich
In:9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020)
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:12476
Part:I: Verification Principles
Year:2020
Pages:60-80
Preprint/PDF:BeckertKirstenEA20.pdf
DOI:10.1007/978-3-030-61362-4_4

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.
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.

BibTeX

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