The SLAM project: Debugging system software via static analysis

被引：191

作者：

Ball, T ^{[1
]}

Rajamani, SK ^{[1
]}

机构：

[1] Microsoft Res, Redmond, WA 98052 USA

来源：

ACM SIGPLAN NOTICES | 2002年 / 37卷 / 01期

关键词：

D O I：

10.1145/565816.503274

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The goal of the SLAM project is to check whether or not a program obeys "API usage rules" that specify what it means to be a good client of an API. The SLAM toolkit statically analyzes a C program to determine whether or not it violates given usage rules. The toolkit has two unique aspects: it does not require the programmer to annotate the source program (invariants are inferred); it minimizes noise (false error messages) through a process known as "counterexample-driven refinement". SLAM exploits and extends results from program analysis, model checking and automated deduction. We have successfully applied the SLAM toolkit to windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.

引用

页码：1 / 3

页数：3