Model Checking for UNITY
Markus Kaltenbach · 1994
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.