Treffer: Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Heuristics for Model Checking Java Programs

The date of receipt and acceptance will be inserted by the editor Abstract. Model checking of software programs has two goals: one is the verification of correct software. The other is the discovery of errors in faulty software. Some techniques for dealing with the most crucial problem in model checking, the state space explosion problem, concentrate on the first of these goals. In this paper we present an array of heuristic model checking techniques for combating the state space explosion when searching for errors. Previous work on this topic has mostly focused on property-specific heuristics closely related to particular kinds of errors. We present structural heuristics that attempt to explore the structure (branching structure, thread inter-dependency structure, abstraction structure) of a program in a manner intended to expose errors efficiently. Experimental results show the utility of this class of heuristics. In contrast to these very general heuristics, we also present very lightweight techniques for introducing program-specific heuristic guidance. 1