Correctness of Efficient Real-Time Model Checking
Wolfgang Reif (University of Augsburg, Germany)
Gerhard Schellhorn (University of Augsburg, Germany)
Tobias Vollmer (University of Augsburg, Germany)
Jürgen Ruf (University of Tübingen, Germany)
Abstract: 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.
Keywords: correctness proofs, interactive theorem proving, invariants, model checking, optimization techniques, program verification, structured algebraic specifications, temporal logic
Categories: D.2.1, D.2.4, F.3.1, F.3.2, F.4.1