Bandera: extracting finite-state models from Java source code

By J. Corbett, Matthew B. Dwyer, J. Hatcliff, S. Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng. Proceedings of the 2000 International Conference on Software Engineering. ICSE 2000 the New Millennium, 2000

1,284 citations recorded by the source corpus.

Finite-state verification techniques, such as model checking, have shown promise as a cost-effective means for finding defects in hardware designs. To date, the application of these techniques to software has been hindered by several obstacles. Chief among these is the problem of constructing a finite-state model that approximates the executable behavior of the software system of interest. Current best-practice involves hand construction of models which is expensive (prohibitive for all but the smallest systems), prone to errors (which can result in misleading verification results), and difficult to optimize (which is necessary to combat the exponential complexity of verification algorithms). The authors describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models from program source code. Bandera takes as input Java source code and generates a program model in the input language of one of several existing verification tools; Bandera also maps verifier outputs back to the original source code. We discuss the major components of Bandera and give an overview of how it can be used to model check correctness properties of Java programs.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/4f70fc6702080f98e9f5a994109e03ecb3d2bf1f

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Software

Citations in the corpus

The software model checker Blast (2007, background): “Software model checking, the application of algorithmic verification to implemented code, has been an active area of recent research [4,17,28,35,42, 52,66].”
Software model checking (2009, positive): “They were also used as back-ends for initial attempts at software model checking [Corbett et al. 2000].”
Extended static checking for Java (2002, methodology): “[5] J. Corbett et al. Bandera: Extracting .nite-state models from Java source code.”
Checking system rules using system-specific, programmer-written compiler extensions (2000, background): “While recent work has begun attacking these problems [6, 14], it is extremely rare for software to be veri ed.”
Using formal specifications to support testing (2009, methodology): “Model-checking using abstraction is described in [Corbett et al. 2000; Holzmann and Smith 2001].”
The SPIN Model Checker - primer and reference manual (2003, neutral): “, Cousot and Cousot [1976]. A detailed discussion of the theoretical background for abstraction is well beyond the scope of this book, but a good starting point for such a discussion can be found in, for instance, the work of Abadi and Lamport [1991], Kurshan [1993], Clarke, Grumberg, and Long [1994”
TestEra: a novel framework for automated testing of Java programs (2001, methodology): “The Bandera project [6] provides automated support for reducing a programs state space through program slicing and data abstraction.”
Effective typestate verification in the presence of aliasing (2006, methodology): “RELATED WORK Many existing veri.cation frameworks [Das et al. 2002; Ball et al. 2001; Corbett et al. 2000] use a two-phased approach, performing points-to analysis as a preceding phase, followed by typestate checking.”
EXE: automatically generating inputs of death (2006, methodology): “7.2 Software Model Checking Model checkershavebeenused to .ndbugsinboth thedesignand theimplementation of software[Holzmann1997,2001;Brat et al.2000;Corbett et al. 2000; Ball and Rajamani 2001; Godefroid 1997; Yang et al. 2004].”
Semantics-aware malware detection (2005, result): “In a larger context, our work is similar to existing research on software verification [2,11].”
Test input generation with java PathFinder (2004, methodology): “More recently the application of model checking to the analysis of software programs has also come to the fore [7,15,27,43].”
Synthesis of interface specifications for Java classes (2005, methodology): “A relevant line of research is the recent work on software verification tools such as Bandera [13], SLAM [6], Feaver [22], and Blast [21].”