Integration of Bounded Model Checking and Deductive Verification
Bernhard Beckert, Thorsten Bormer, Florian Merz, and Carsten Sinz
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.