A Decade of Software Model Checking with SLAM

by Thomas Ball , Vladimir Levin, and Sriram K. Rajamani
communications of the acm | july 2011 | vol. 54 | no. 7

remark: SLAM is a program-analysis engine used to check if clients of an API follow the API's stateful usage rules.

key insights

• Even though programs have many states, it is possible to construct an abstraction of a program fine enough to represent parts of a program relevant to an API usage rule and coarse enough for a model checker to explore all the states.
• SLAM synthesizes and extends diverse ideas from model checking, theorem proving, and data-flow analysis to
  automate construction, checking, and refinement of abstractions.
• SLAM showed that such abstractions can be constructed automatically for real-world programs, becoming the basis of Microsoft’s Static Driver Verifier tool.

SLAM

question: whether API rules can be formally documented so programs using the APIs can be checked at compile time for compliance against the rules.

SLAM

SLIC specification language.

specificiation example

CEGAR via predicate abstraction.

Figure 2 presents ML-style pseudocode of the CEGAR process.

CEGAR procedure

The goal of SLAM is to check if all executions of the
given C program P (type cprog) satisfy a
SLIC rule S (type spec).

abstract (P´, preds ∪ refine(pr f))

From SLAM to SDV

SDV: a completely automatic tool (based on SLAM) device-driver developers can use at compile time.

remark: We wanted to build a verifier covering
all possible behaviors of the program while checking the rule, as opposed to a testing tool that checks the rule on a
subset of behaviors covered by the test.

Environment models.

Related Work

• Model checking15,16,41
• predicate abstraction

Conclusion

A unique SLAM contribution: the complete automation of CEGAR for software written in expressive programming languages (such as C).