NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Foundations of the Bandera Abstraction ToolsCurrent research is demonstrating that model-checking and other forms of automated finite-state verification can be effective for checking properties of software systems. Due to the exponential costs associated with model-checking, multiple forms of abstraction are often necessary to obtain system models that are tractable for automated checking. The Bandera Tool Set provides multiple forms of automated support for compiling concurrent Java software systems to models that can be supplied to several different model-checking tools. In this paper, we describe the foundations of Bandera's data abstraction mechanism which is used to reduce the cardinality (and the program's state-space) of data domains in software to be model-checked. From a technical standpoint, the form of data abstraction used in Bandera is simple, and it is based on classical presentations of abstract interpretation. We describe the mechanisms that Bandera provides for declaring abstractions, for attaching abstractions to programs, and for generating abstracted programs and properties. The contributions of this work are the design and implementation of various forms of tool support required for effective application of data abstraction to software components written in a programming language like Java which has a rich set of linguistic features.
Document ID
20030022709
Document Type
Preprint (Draft being sent to journal)
Authors
Hatcliff, John (Kansas State Univ. Manhattan, KS, United States)
Dwyer, Matthew B. (Kansas State Univ. Manhattan, KS, United States)
Pasareanu, Corina S. (Kestrel Technology, LLC Moffett Field, CA, United States)
Robby (Kansas State Univ. Manhattan, KS, United States)
Date Acquired
September 7, 2013
Publication Date
January 1, 2003
Subject Category
Computer Programming and Software
Funding Number(s)
CONTRACT_GRANT: NSF CCR-97-08184
CONTRACT_GRANT: NCC1-399
CONTRACT_GRANT: NSF CCR-97-03094
CONTRACT_GRANT: F33615-00-C-3044
CONTRACT_GRANT: NSF CCR-98-96354
CONTRACT_GRANT: NSF CCR 99-01605
CONTRACT_GRANT: NAS2-00065
CONTRACT_GRANT: DAAD19-01-110564
CONTRACT_GRANT: NAG2-1209
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Available Downloads

NameType 20030022709.pdf STI