Model checking programs

The majority of work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal meth-ods such as theorem provers and model checkers. In this paper we will attempt to give convincing arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy we have developed a verification and testing environment for Java, Java PathFinder (JPF), which inte-grates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state com-pression to handle big states, and partial order reduction, slicing, abstraction, and runtime analysis techniques to re-duce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illus-trating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, run-time analysis, and slicing with model checking.