Treffer: Model checking Java programs using structural heuristics
Title:
Model checking Java programs using structural heuristics
Authors:
Source:
ACM SIGSOFT Software Engineering Notes ; volume 27, issue 4, page 12-21 ; ISSN 0163-5948
Publisher Information:
Association for Computing Machinery (ACM)
Publication Year:
2002
Document Type:
Fachzeitschrift
article in journal/newspaper
Language:
English
DOI:
10.1145/566171.566175
Availability:
Accession Number:
edsbas.5950CE1B
Database:
BASE
Weitere Informationen
We describe work in troducing heuristic search into the Java PathFinder model checker, which targets Java bytecode. Rather than focusing on heuristics aimed at a particular kind of error (such as deadlocks) we describe heuristics based on a modification of traditional branch coverage metrics and other structure measures, such as thread inter-dependency. We present experimental results showing the utility of these heuristics, and argue for the usefulness of structural heuristics as a class.