Model Checking for UNITY

Abstract

We present a description of our current implementation of a model checker for finite state UNITY programs and propositional UNITY logic. The model checker is capable of dealing with all unconditional properties of UNITY logic. Checking safety properties and basic progress properties can be done very efficiently due to the partitioning of the transition relation of a program induced by the program statements. Finding suitable invariants remains a crucial task in proving properties. The model checker provides means for both computing the strongest invariant of a program and for managing established invariants.

This page was last updated on 7-December-1994

Markus Kaltenbach (markus@cs.utexas.edu)