The SLAM project, which was started by Microsoft Research, aimed at verifying some software safety properties using model checking techniques. It is implemented in Ocaml, and has been used to find many bugs in Windows Device Drivers. It is distributed as part of the Microsoft Windows Driver Foundation development kit as the Static Driver Verifier (SDV).

SLAM uses a technique called counterexample-guided abstraction refinement, which uses progressively better models of the program under test.

“SLAM originally was an acronym but we found it too cumbersome to explain. We now prefer to think of ‘slamming’ the bugs in a program.” It probably stood for “Software, Languages, Analysis, and Modeling.” Note that Microsoft has since re-used SLAM to stand for “Social Location Annotation Mobile”

About Abstraction Methods:

There are three ways to abstract programs.

  1. Over-abstract like abstract interpretation
  2. Under-abstraction like SLAM, also called meat-axe – abstraction, which cuts of some information
  3. Precise abstraction which is the best description for Symbolic Analysis (Laitila), which uses the Symbolic language for that.

Because SLAM removes some information, it is not complete to describe program comprehension features of the program, which include: control flow, data flow, state flow, operations and full functionality (Pennington, Wiedenbeck, von Mayrhauser et al.).

Paper X describes counterexample-guided abstraction refinement with some methods:

There is a traffic light example in it to model states.

Some algorithms in the paper are SPLITPath, PolyRefine and SPLITLoop.

Precice abstraction in Symbolic Analysis

We define precise abstraction as a formula M <– –> M’, where M is the original model (or code) containing Java, C++ or other language and M’ is the abstracted model with AHO objects, where the command from each AHO has been transformed according to the original grammar term of the corresponding program element. The abstracted model can be transformed back into the original language. Thus, the model is reversible.

Some links:

Advertisements