Heuristics for model checking Java programs

Alex Groce, Willem Visser

Research output: Contribution to journalArticlepeer-review

69 Scopus citations

Abstract

Model checking of software programs has two goals - the verification of correct software and 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 interdependency 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.

Original languageEnglish (US)
Pages (from-to)260-276
Number of pages17
JournalInternational Journal on Software Tools for Technology Transfer
Volume6
Issue number4
DOIs
StatePublished - 2004
Externally publishedYes

Keywords

  • Coverage metrics
  • Heuristic search
  • Model checking
  • Testing

ASJC Scopus subject areas

  • Software
  • Information Systems

Fingerprint

Dive into the research topics of 'Heuristics for model checking Java programs'. Together they form a unique fingerprint.

Cite this