Abstract Model Checking of Infinite Specifications

Model Checking of Infinite Specifications Daniel Jackson School of Computer Science Carnegie Mellon University Pittsburgh, PA A new method for analyzing specifications in languages like Z and VDM is proposed. Theorems are checked automatically by exhaustive search of the state space. An abstraction over the actual states can be defined that reduces an infinite state space to a finite number of equivalence classes, allowing searched exhaustively by treating each class as a single abstract state. A prototype has been built that has verified some small theorems from the literature. If ifs and ands were pots and pans, There'd be no need for tinkers hands --Mother Goose

• Type: Conference
• Year: 1994
• Where: FM
• Authors: Daniel Jackson
• Keywords: FM 1994, Formal Methods, Infinite State Space, Specifications Daniel Jackson, State Space