The SLAM Toolkit

The SLAM toolkit checks safety properties of software without the need for user-supplied annotations or abstractions. Given a safety property to check on a C program P, the SLAM process [4] iteratively refines a boolean program abstraction of P using three tools: - C2bp, a predicate abstraction tool that abstracts P into a boolean program BP(P,E) with respect to a set of predicates E over P1,2;- BEBOP, a tool for model checking boolean programs [3], and- NEWTON, a tool that discovers additional predicates to refine the boolean program, by analyzing the feasibility of paths in the C program.