Correctness of Efficient Real-Time Model Checking.
Wolfgang Reif, Gerhard Schellhorn, Tobias Vollmer, Jürgen Ruf · Zenodo (CERN European Organization for Nuclear Research) · 2001
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.