MODEL CHECKING AND ABSTRACTION

被引：622

作者：

CLARKE, EM

GRUMBERG, O

LONG, DE

机构：

[1] TECHNION ISRAEL INST TECHNOL,DEPT COMP SCI,IL-32000 HAIFA,ISRAEL

[2] AT&T BELL LABS,MURRAY HILL,NJ 07974

来源：

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 1994年 / 16卷 / 05期

关键词：

ABSTRACT INTERPRETATION; BINARY DECISION DIAGRAMS (BDDS); MODEL CHECKING; TEMPORAL LOGIC;

D O I：

10.1145/186025.186051

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct 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 program representing a pipelined ALU circuit with over 10(1300) states.

引用

页码：1512 / 1542

页数：31

共 33 条

[1]

BEATTY DL, 1991, 28TH P DES AUT C, P397

[2]

BENSALEM S, 1992, LECT NOTES COMPUTER, V663, P260

[3]

BROWNE MC, 1986, IEEE T COMPUT, V35, P1035, DOI 10.1109/TC.1986.1676711

[4]

BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819

[5]

Burch J. R., 1990, 27th ACM/IEEE Design Automation Conference. Proceedings 1990 (Cat. No.90CH2894-4), P46, DOI 10.1109/DAC.1990.114827

[6]

BURCH JR, 1991, 28TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, P403, DOI 10.1145/127601.127702

[7] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].

CLARKE, EM ;

EMERSON, EA ;

SISTLA, AP .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263

[8]

CLARKE EM, 1983, 10TH ACM S PRINC PRO, P117

[9]

CLARKE EM, 1989, 4TH P ANN S LOG COMP, P46

[10]

CLARKE EM, 1981, LECTURE NOTES COMPUT, V131

← 1 2 3 4 →