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

Corresponding author: Wolfgang Reif ( reif@informatik.uni-augsburg.de )

© Wolfgang Reif, Gerhard Schellhorn, Tobias Vollmer, Jürgen Ruf.
This article is freely available under the J.UCS Open Content License.
Citation: Reif W, Schellhorn G, Vollmer T, Ruf J (2001) Correctness of Efficient Real-Time Model Checking. JUCS - Journal of Universal Computer Science 7(2): 194-209. https://doi.org/10.3217/jucs-007-02-0194
Open Access
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
model checking, interactive theorem proving, structured algebraic specifications, correctness proofs, program verification, optimization techniques, invariants, temporal logic