contributed articles

DoI: 10.1145/1965724.1965743

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

BY ThoMAS BALL, VLADIMIR LEVIn, AnD SRIRAM K. RAJAMAnI A Decade of Software Model Checking with SLAM

LArGe-sCALe sOFt WAre 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

spinlock must be done in strict alternation and the rule that a file can be read only after it is opened. We built the SLAM engine (SLAM from now on) to allow programmers to specify stateful usage rules and statically check if clients follow such rules. We wanted SLAM to be scalable and at the same time have a very low false-error rate. To scale the SLAM engine, we constructed abstractions that retain only information about certain predicates related to the property being checked. To reduce false errors, we refined abstractions automatically using counterexamples from the model checker. Constructing and refining abstractions for scaling model checking has been known for more than 15 years; Kurshan35 is the earliest reference we know.

SLAM automated the process of abstraction and refinement with counterexamples for programs written in common programming languages (such as C) by introducing new techniques to handle programming-language constructs (such as pointers, procedure calls, and scoping constructs for variables). 2, 4–8 Independently and simultaneously with our work, Clarke et al. 17 automated abstraction and refinement with counterexamples in the context of hardware, coining the term “counterexample-driven abstraction refinement,” or CEGAR, which we use to refer to this technique throughout

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.