JUCS - Journal of Universal Computer Science 7(2): 194-209, doi: 10.3217/jucs-007-02-0194
Correctness of Efficient Real-Time Model Checking
expand article infoWolfgang Reif, Gerhard Schellhorn§, Tobias Vollmer§, Jürgen Ruf|
‡ University of Augsburg, Augsburg, Germany§ University of Augsburg, Germany| University of Tübingen, Tübingen, Germany
Open Access
In this paper we describe the formal specification and verification of an efficient algorithm based on bitvectors for real-time model checking with the KIV system. We demonstrate that the verification captures the essentials of the C++ algorithm as implemented in the RAVEN model checker. Verification revealed several possibilities to reduce the size of the code and to improve its efficiency.
model checking, interactive theorem proving, structured algebraic specifications, correctness proofs, program verification, optimization techniques, invariants, temporal logic