Name
Abstract | ||
|---|---|---|
Modular deductive verification of software systems is a complex task: the user has to put a lot of effort in writing module specifications that fit together when verifying the system as a whole. In this paper, we propose a combination of deductive verification and software bounded model checking (SBMC), where SBMC is used to support the user in the specification and verification process, while deductive verification provides the final correctness proof. SMBC provides early --- as well as precise --- feedback to the user. Unlike modular deductive verification, the SBMC approach is able to check annotations beyond the boundaries of a single module --- even if other relevant modules are not annotated (yet). This allows to test whether the different module specifications in the system match the implementation at every step of the specification process. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-31762-0_7 | FoVeOOS |
Keywords | Field | DocType |
software system,sbmc approach,deductive verification,software bounded model checking,verification process,modular deductive verification,module specification,relevant module,single module,different module specification | Functional verification,Programming language,Model checking,Computer science,Theoretical computer science,Verification,Software system,Software,Symbolic execution,Modular design,Class invariant | Conference |
Citations | PageRank | References |
2 | 0.38 | 18 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernhard Beckert | 1 | 862 | 86.50 |
| Thorsten Bormer | 2 | 58 | 4.90 |
| Florian Merz | 3 | 151 | 9.56 |
| Carsten Sinz | 4 | 787 | 46.29 |