Using Runtime Analysis to Guide Model Checking of Java Programs

10 years 2 months ago
Using Runtime Analysis to Guide Model Checking of Java Programs
This paper describes how two runtime analysis algorithms, an existing data race detection algorithm and a new deadlock detection algorithm, have been implemented to analyze Java programs. Runtime analysis is based on the idea of executing the program once, and observing the generated run to extract various kinds of information. This information can then be used to predict whether other di erent runs may violate some properties of interest, in addition of course to demonstrate whether the generated run itself violates such properties. These runtime analyses can be performed stand-alone to generate a set of warnings. It is furthermore demonstrated how these warnings can be used to guide a model checker, thereby reducing the search space. The described techniques have been implemented in the home grown Java model checker called Java PathFinder. KeywordsConcurrent programs, runtimeanalysis, race conditions, deadlocks, program veri cation, guided model checking, Java.
Klaus Havelund
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where SPIN
Authors Klaus Havelund
Comments (0)