Model checking and abstraction

1 January 1992

proceedings article
Published by Association for Computing Machinery (ACM)

p. 343-354
https://doi.org/10.1145/143165.143235

Abstract

We describe a method for using abstraction to reduce the complexity of temporal logic model checking. The basis of this method is a way of constructing an abstract model of a program 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 techniques, and we demonstrate their practicality using a number of examples, including a pipelined ALU circuit with over 101300 states.

Keywords

TEMPORAL LOGLC
ORIGINAL PROGRAM
ADDLTLONAL KEY WORDS AND PHRASES: ABSTRACT MTERPRETATLON
ABSTRACT MODEL
MODEL CHECKING
PIPELINED ALU CIRCUIT
CORRESPONDING UNABSTRACTED MODEL
TEMPORAL LOGIC MODEL CHECKING
BINARY DECLSLON DIAGRAMS BDDS
PARTIAL EVALUATION
TEMPORAL LOGIC

This publication has 0 references indexed in Scilit: