Software Model Checking

被引：229

作者：

Jhala, Ranjit ^{[1
]}

Majumdar, Rupak ^{[2
]}

机构：

[1] Univ Calif San Diego, Dept Comp Sci & Engn, La Jolla, CA 92093 USA

[2] Univ Calif Los Angeles, Los Angeles, CA USA

来源：

ACM COMPUTING SURVEYS | 2009年 / 41卷 / 04期

基金：

美国国家科学基金会;

关键词：

Languages; Verification; Reliability; Software model checking; enumerative and symbolic model checking; abstraction; counterexample-guided refinement; safety; liveness; MODULAR VERIFICATION; CONCURRENT PROGRAMS; ABSTRACTION; GUARANTEE; SAFETY; COMPLETENESS; TERMINATION; INDUCTION; ALGORITHM; SYMMETRY;

D O I：

10.1145/1592434.1592438

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We survey recent progress in software model checking.

引用

页数：54

共 236 条

[1] COMPOSING SPECIFICATIONS [J].

ABADI, M ;

LAMPORT, L .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1993, 15 (01) :73-132

[2] CONJOINING SPECIFICATIONS [J].

ABADI, M ;

LAMPORT, L .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1995, 17 (03) :507-534

[3]

AGERWALA T, 1978, 83 U TEX

[4]

Allen Emerson E., 1986, LICS, P267

[5] RECOGNIZING SAFETY AND LIVENESS [J].

ALPERN, B ;

SCHNEIDER, FB .

DISTRIBUTED COMPUTING, 1987, 2 (03) :117-126

[6] Counterexample-guided predicate abstraction of hybrid systems [J].

Alur, R ;

Dang, T ;

Ivancic, F .

THEORETICAL COMPUTER SCIENCE, 2006, 354 (02) :250-271

[7] TIMING VERIFICATION BY SUCCESSIVE APPROXIMATION [J].

ALUR, R ;

ITAI, A ;

KURSHAN, RP ;

YANNAKAKIS, M .

INFORMATION AND COMPUTATION, 1995, 118 (01) :142-157

[8] Reactive modules [J].

Alur, R ;

Henzinger, TA .

FORMAL METHODS IN SYSTEM DESIGN, 1999, 15 (01) :7-48

[9]

Alur R, 1998, LECT NOTES COMPUT SC, V1427, P521, DOI 10.1007/BFb0028774

[10]

Andersen L. O, 1994, THESIS CITESEER

← 1 2 3 4 5 6 7 8 9 10 →