Semi-automatic Predicate Abstraction of Sequential Programs

Model checking can be applied to software systems to check the reachability of a particular state. As model checking suffers from the state explosion problem, abstract models of software systems must be formed to make model checkers able to overcome this limitation. We have developed J2, a tool that incorporates some refined techniques to construct a predicate abstraction of sequential programs written in Java, i.e. boolean programs. We also demonstrate the use of a model checker named BEBOP developed by Microsoft Research to model check those programs