Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 7 / Issue 2

available in:   PDF (228 kB) PS (87 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-007-02-0194


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