Tool-Support Program Abstraction
Abstraction is a fundamental step in the construction of models for software systems. The abstraction techniques used in Bandera are based on abstraction-based program specialization (ABPS): a combination of abstract interpretation and partial evaluation technologies.
To construct an abstract model of a software system using ABPS, the model designer associates each program variable with an abstraction class. An abstraction class is an abstract version of a regular concrete Java class. The abstraction class abstracts away from various details of the original Java class and only retains information that is relevant for the particular software specification to be verified. For example, a stack class might be abstracted so that only information about the stack's size is retained (the actual contents are abstracted away).
Abstraction classes are defined using the Bandara Abstraction Specification Language (BASL). The BASL compiler translates a BASL specification to the Java implementation of the specified abstraction class. Compiled abstraction class are held in a library, allowing the model designer to easily reuse common abstractions.
- Tool-supported Program Abstraction for Finite-state Verification, Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, Hongjun Zheng, in Proceedings of the 23rd International Conference on Software Engineering, May, 2001. (to appear).
- Data-flow analysis as model checking of abstract interpretations. David A. Schmidt and Bernhard Steffen Invited tutorial paper, Proc. 5th Static Analysis Symposium, G. Levi. ed., Pisa, September, 1998. Springer LNCS 1503.
- Staging Static Analyses Using Abstraction-based Program Specialization , John Hatcliff, Matthew B. Dwyer, Shawn Laubach. This paper is published as KSU CIS TR 98-5 and a more compact version appeared in LNCS 1490 (Principles of Declarative Programming: 10th International Symposium, PLILP'98), September, 1998.
- Using Partial Evaluation to Enable Verification of Concurrent Software, Matthew B. Dwyer, John Hatcliff, and Muhammad Nanda This paper is published as KSU CIS TR 97-15 and will appear in ACM Computing Surveys. An abstract of this paper is also available.
- Specializing Configurable Systems for Finite-state Verification , John Hatcliff, Matthew B. Dwyer, Shawn Laubach, and Nanda Muhammad. This paper is published as KSU CIS TR 98-4 and has been submitted for publication. An abstract of this paper is also available.
- Data-flow analysis is model checking of abstract interpretations. David A. Schmidt. Proc. 25th ACM Symp. Principles of Programming Languages, San Diego, 1998.