/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96
"/> KIT - Application-oriented Formal Verification - <br /> <b>Warning</b>: Undefined array key "title" in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br /> <br /> <b>Warning</b>: Attempt to read property "value" on null in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br />
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.