The goal of the SLAMproject 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 SLAMtoolkit 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". SLAMexploits and extends results from program analysis, model checking and automated deduction. We have successfully applied the SLAMtoolkit to Windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.
No takes yet. Share an insight, caveat, or question.
Ball et al. (2002) studied this question.
Synapse has enriched 4 closely related papers on similar clinical questions. Consider them for comparative context: