MODEL CHECKING AND ABSTRACTION

Authors
CLARKE EM GRUMBERG O LONG DE
Citation
Em. Clarke et al., MODEL CHECKING AND ABSTRACTION, ACM transactions on programming languages and systems, 16(5), 1994, pp. 1512-1542
Citations number
33
Categorie Soggetti
Computer Sciences","Computer Science Software Graphycs Programming
Journal title
ACM transactions on programming languages and systems → ACNP
ISSN journal
01640925
Volume
16
Issue
5
Year of publication
1994
Pages
1512 - 1542
Database
ISI
SICI code
0164-0925(1994)16:5<1512:MCAA>2.0.ZU;2-U
Abstract
We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those invo lved in abstract interpretation, we construct an abstract model of a p rogram without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniqu es, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10( 1300) states.