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