DocumentCode
2486187
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
fYear
2000
fDate
2000
Firstpage
253
Lastpage
256
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Automated Software Engineering, 2000. Proceedings ASE 2000. The Fifteenth IEEE International Conference on
Conference_Location
Grenoble
ISSN
1938-4300
Print_ISBN
0-7695-0710-7
Type
conf
DOI
10.1109/ASE.2000.873671
Filename
873671
Link To Document