zbMATH — the first resource for mathematics

Using runtime analysis to guide model checking of Java programs. (English) Zbl 0976.68576
Havelund, Klaus (ed.) et al., SPIN model checking and software verification. 7th international SPIN workshop, Stanford, CA, USA, August 30 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1885, 245-264 (2000).
Summary: 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 different 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.
For the entire collection see [Zbl 0947.00033].

68U99 Computing methodologies and applications
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)