Model checking Java programs using structural heuristics

Alex Groce, Willem Visser

Research output: Chapter in Book/Report/Conference proceedingConference contribution

62 Scopus citations

Abstract

We describe work introducing heuristic search into the Java PathFinder model checker, which targets Java bytecode1. 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 structural 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.

Original languageEnglish (US)
Title of host publicationProceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis
EditorsP.G. Frankl
PublisherAssociation for Computing Machinery (ACM)
Pages12-21
Number of pages10
ISBN (Print)1581135629, 9781581135626
DOIs
StatePublished - 2002
Externally publishedYes
EventISSTA 02 Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis - Roma, Italy
Duration: Jul 22 2002Jul 24 2002

Publication series

NameProceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis

Conference

ConferenceISSTA 02 Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis
Country/TerritoryItaly
CityRoma
Period7/22/027/24/02

Keywords

  • Coverage metrics
  • Heuristics
  • Model checking
  • Testing

ASJC Scopus subject areas

  • General Engineering

Fingerprint

Dive into the research topics of 'Model checking Java programs using structural heuristics'. Together they form a unique fingerprint.

Cite this