Do You Trust Your Model Checker?

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.

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn, Tobias Vollmer
• Keywords: Corresponding Verification Efforts, FMCAD 2000, Formal Methods, Formal Verification, Model Checker Raven