Java model checking

1 January 2000

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 253
https://doi.org/10.1109/ase.2000.873671

Abstract

This paper presents initial results in model checking multi-threaded Java programs. Java programs are translated into the Sal (Symbolic Analysis Laboratory) intermediate language, which supports dynamic constructs such as objects instantiations and thread call stacks. The SAL model checker then exhaustively checks the program description for deadlocks and assertion failures, using traditional model checking optimizations to curb the state explosion problem. Most of the advanced features of the Java language are modeled within our framework.

Keywords

This publication has 8 references indexed in Scilit:

Bandera: extracting finite-state models from Java source code
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
Type-based race detection for Java
Published by Association for Computing Machinery (ACM) ,2000
Model checking JAVA programs using JAVA PathFinder
International Journal on Software Tools for Technology Transfer, 2000
A deadlock detection tool for concurrent Java programs
Software: Practice and Experience, 1999
Eraser
ACM Transactions on Computer Systems, 1997
The model checker SPIN
IEEE Transactions on Software Engineering, 1997
The Mur ϕ verification system
Published by Springer Nature ,1996
Partial-Order Methods for the Verification of Concurrent Systems
Published by Springer Nature ,1996