kirancodes.me
To Proof Maintenance & Beyond!
ICSE 2001

Tool-Supported Program Abstraction for Finite-State Verification

Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng, Willem Visser

DOI 10.1109/icse.2001.919092dblp

Abstract

Numerous researchers have reported success in reasoning about properties of small programs using finite-state verification techniques. We believe, as do most researchers in this area, that in order to scale those initial successes to realistic programs, aggressive abstraction of program data will be necessary. Furthermore, we believe that to make abstraction-based verification usable by non-experts significant tool support will be required. In this paper we describe how several different program analysis and transformation techniques are integrated into the Bandera toolset to provide facilities for abstracting Java programs to produce compact, finite-state models that are amenable to verification for example via model checking. We illustrate the application of Bandera's abstraction facilities to analyze a realistic multi-threaded Java program.

BibTeX
@inproceedings{Dwyer-al:ICSE01,
  author    = {Matthew B. Dwyer and
               John Hatcliff and
               Roby Joehanes and
               Shawn Laubach and
               Corina S. Pasareanu and
               Robby and
               Hongjun Zheng and
               Willem Visser},
  title     = {{Tool-Supported} Program Abstraction for {Finite-State} Verification},
  booktitle = {ICSE},
  pages     = {177--187},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Related papers