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 条

[51]

BLANCHET B, 2003, P ACM SIGPLAN 2003 C, P196, DOI [DOI 10.1145/780822.781153, 10.1145/781131.781153, DOI 10.1145/781131.781153]

[52] A generic approach to the static analysis of concurrent programs with procedures [J].

Bouajjani, A ;

Esparza, J ;

Touili, T .

ACM SIGPLAN NOTICES, 2003, 38 (01) :62-73

[53]

BOUAJJANI A, 1991, LECT NOTES COMPUT SC, V531, P197, DOI 10.1007/BFb0023733

[54]

BOUAJJANI A, 1994, LECT NOTES COMPUTER, V1243, P135

[55]

Bradley AR, 2005, LECT NOTES COMPUT SC, V3580, P1349

[56]

BRAT G, 2004, FORM METH SYST DES, V25

[57]

Bruttomesso R, 2008, LECT NOTES COMPUT SC, V5123, P299

[58]

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

[59] SYMBOLIC MODEL CHECKING - 1020 STATES AND BEYOND [J].

BURCH, JR ;

CLARKE, EM ;

MCMILLAN, KL ;

DILL, DL ;

HWANG, LJ .

INFORMATION AND COMPUTATION, 1992, 98 (02) :142-170

[60] Simulation-based minimization [J].

Bustan, Doron ;

Grumberg, Orna .

ACM Transactions on Computational Logic, 2003, 4 (02) :181-206

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