Do you trust your model checker?

Wolfgang Reif, Juergen Ruf, Gerhard Schellhorn, Tobias Vollmer

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


Abstract

In this paper we describe the formal specification and verification of the efficient algorithm for real-time model checking implemented in the model checker RAVEN. It was specified and proved using the KIV system. We demonstrate how to decompose the correctness proof into several independent subtasks and indicate the corresponding verification efforts. The formal verification revealed some errors, reduced the code size, and improved the efficiency of the implementation.


Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:37
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems