Modular Verification of JML Contracts Using Bounded Model Checking
| Autor: | Jonas Klamroth, Michael Kirsten, Mattias Ulbrich, Bernhard Beckert |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Model checking
050101 languages & linguistics Java Computer science 02 engineering and technology Design by contract computer.software_genre Software verification 0202 electrical engineering electronic engineering information engineering 0501 psychology and cognitive sciences computer.programming_language Modular design Programming language DATA processing & computer science 05 social sciences Software bounded model checking Nondeterministic algorithm Bounded function Modular programming 020201 artificial intelligence & image processing ddc:004 computer Java Modeling Language |
| Zdroj: | Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles ISBN: 9783030613617 ISoLA (1) |
| ISSN: | 1611-3349 |
| DOI: | 10.5445/ir/1000125411 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|