Title :
Java model checking
Author :
Park, David Y W ; Stern, Ulrich ; Skakkebaek, Jens U. ; Dill, David L.
Author_Institution :
Dept. of Comput. Sci., Stanford Univ., CA, USA
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 object 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 :
Java; concurrency control; multi-threading; object-oriented programming; program verification; Java model checking; SAL language; Symbolic Analysis Laboratory language; assertion failure; deadlocks; multithreaded Java programs; object instantiations; optimizations; program description; state explosion problem; thread call stacks; Computer languages; Computer science; Data structures; Explosions; Internet; Java; Laboratories; System recovery; Writing; Yarn;
Conference_Titel :
Automated Software Engineering, 2000. Proceedings ASE 2000. The Fifteenth IEEE International Conference on
Conference_Location :
Grenoble
Print_ISBN :
0-7695-0710-7
DOI :
10.1109/ASE.2000.873671
