Sciweavers

FM
1994
Springer

Abstract Model Checking of Infinite Specifications

13 years 7 months ago
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
Daniel Jackson
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where FM
Authors Daniel Jackson
Comments (0)