A Decade of Software Model Checking with SLAM

被引：111

作者：

Ball, Thomas ^{[1
]}

Levin, Vladimir ^{[2
]}

Rajamani, Sriram K. ^{[3
]}

机构：

[1] Microsoft Res, Software Reliabil Res Grp, Redmond, WA 98052 USA

[2] Microsoft Corp, Stat Driver Verificat Project Windows, Redmond, WA 98052 USA

[3] Microsoft Res India, Bangalore, Karnataka, India

来源：

COMMUNICATIONS OF THE ACM | 2011年 / 54卷 / 07期

关键词：

Application programming interfaces (API);

D O I：

10.1145/1965724.1965743

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

LARGE-SCALE SOFTWARE DEVELOPMENT is a notoriously difficult problem. Software is built in layers, and APIs are exposed by each layer to its clients. APIs come with usage rules, and clients must satisfy them while using the APIs. Violations of API rules can cause runtime errors. Thus, it is useful to consider whether API rules can be formally documented so programs using the APIs can be checked at compile time for compliance against the rules. Some API rules (such as agreement on the number of parameters and data types of each parameter) can be checked by compilers. However, certain rules involve hidden state; for example, consider the rule that the acquire method and release method of a

引用

页码：68 / 76

页数：9

共 45 条

[1] An Overview of the Saturn Project [J].

Aiken, Alex ;

Bugrara, Suhabe ;

Dillig, Isil ;

Dillig, Thomas ;

Hackett, Brian ;

Hawkins, Peter .

PASTE'07 PROCEEDINGS OF THE 2007 ACM SIGPLAN- SIGSOFT WORKSHOP ON PROGRAM ANALYSIS FOR SOFTWARE TOOLS & ENGINEERING, 2007, :43-48

[2]

[Anonymous], 2001, P ACM SIGPLAN 2001 C, DOI DOI 10.1145/378795.378846

[3]

[Anonymous], 2008, NDSS

[4]

[Anonymous], 1981, Lecture Notes in Computer Science, DOI DOI 10.1007/BFB0025774

[5]

[Anonymous], 1993, Symbolic Model Checking

[6] Polymorphic predicate abstraction [J].

Ball, T ;

Millstein, T ;

Rajamani, SK .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005, 27 (02) :314-343

[7]

Ball T., 2001, Tools and Algorithms for the Construction and Analysis of Systems. 7th International Conference, TACAS 2001. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001. Proceedings (Lecture Notes in Computer Science Vol.2031), P268

[8]

Ball T, 2000, LECT NOTES COMPUT SC, V1885, P113

[9]

Ball T., 2001, MSRTR200121

[10]

BALL T, 2000, MSRTR200014

← 1 2 3 4 5 →