Data Abstraction without Control Abstraction in Software Model Checking


June 22, 2006


Michael Jones


Brigham Young University


Data abstraction through predicate abstraction in software model checking requires a theorem proving step to create an abstract version of the program control structure. While this process is effective for programs with simple data manipulations, such as device drivers, abstraction of program control structures can become undecidable and imprecise for more complex, yet reasonable, data manipulations–such as the multiplication of two variables. Data abstractions that do not require the abstraction of program control structures can be applied in the presence of arbitrarily complex data manipulations and support a new method for model checking component- based software.

We discuss two such data abstractions. The first is an extension of static dead variable analysis which allows the use of verification- time information to mark more variables dead during verification. In ideal cases, the resulting analysis yields a 75% reduction in the time and space required for model checking. The second application, which is still being developed, is the use of under-approximating predicate abstraction to abstract the component being verified rather than the surrounding software. This approach to software model checking, when combined with an explicit model checker that operates directly on the software artifact (such as the Java PathFinder), may support the verification of more complex components because the surrounding software can be efficiently and deterministically executed while the component is verified in an abstract data domain. In this setting, data abstraction without control abstraction allows the efficient transfer of control between the abstracted component and surrounding software.


Michael Jones

Michael Jones is an Assistant Professor in the Computer Science Department at Brigham Young University in Provo, Utah. His primary research interest is software model checking and he received the PhD in Computer Science from the University of Utah in 2002.