Java Model Checking

David Y. W. Park, Ulrich Stern, Jens U. Skakkebæk, David L. Dill

DOI 10.1109/ase.2000.873671 dblp

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.

BibTeX

@inproceedings{Park-al:ASE00,
  author    = {David Y. W. Park and
               Ulrich Stern and
               Jens U. Skakkeb{\ae}k and
               David L. Dill},
  title     = {Java Model Checking},
  booktitle = {ASE},
  pages     = {253--256},
  publisher = {{IEEE} Computer Society},
  year      = {2000},
}

Java Model Checking

Abstract

Related papers