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.
