Model Construction for Finite-state Verification

Application of Abstract Interpretation and Partial Evaluation Techniques


ProjectTitleLine:
Model Construction for Finite-state Verification :
Application of Abstract Interpretation and Partial Evaluation Techniques
Period:
01 April 1998 through 1 April 2000
Grant Number:
NASA NAG-2-1209
Investigators:
Matthew Dwyer, John Hatcliff, David A. Schmidt
InstitutionLine:
Kansas State University
POC:
schmidt@cis.ksu.edu
Objective:
In this project we investigate solutions of three fundamental problems hindering the application of finite-state verification (``model checking'') techniques to software: We attack these problems by employing new technology based on the maturing formal-methods techniques of abstract interpretation and partial evaluation: Our methodology liberates the software designer from the burden of designing by hand ad-hoc, potentially incorrect, abstract models of software systems. It also allows the separation-of-concerns of model creation from model checking, meaning that the optimal model checker can be selected for checking a specific class of models.

In addition, the robustness of partial evaluation technology allows it to be applied to modular or ``open'' programs, advancing the frontier of compositional model checking.

We also envisage that our integration of abstract interpretation and partial evaluation machinery will let us undertake serious application of radical state-space reduction techniques based on semantically pseudo-safe abstractions, where symbolic execution undertaken by abstract interpretation might be semantically unsound for some program properties, but it is semantically sound for the correctness properties of interest to the software designer.


Project Reports

For technical details see the Bandera Project.


Project Publications

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.


Related Links


Prepared by Matthew Dwyer (dwyer@cis.ksu.edu), 8 Feb 1999