Reasoning about Changing Software

Project members:

Benet Devereux

Description:

A drawback to traditional formal methods is that they depend upon a static set of requirements and a reasonably unchanging software artifact to be verified against those requirements. In situations where requirements change constantly, as is normal in real world software engineering, the use of currently existing formal methods requires that verification be redone from scratch whenever the software artifact is changed to meet changes in requirements. Our goal is to make formal methods more change-aware, and develop techniques that allow for the re-use of verification results across changes to programs. We focus on model-checking, a highly automated verification method which has seen greatly increased industrial use in the past decade.

Most relevant publications

Benet Devereux, "Compositional Reasoning About Aspects Using Alternating-time Logic", Workshop on Foundations of Aspect Languages (FOAL 2003), Boston, MA, March 2003.
Arie Gurfinkel, Marsha Chechik, Proof-Like Counter-Examples, Proceedings of TACAS'03, April 2003.

Goals:

A number of verification artifacts can be reused. In particular, we are interested in:

Regression verification: here we are trying to see whether existing properties continue to hold in the system, and whether they hold "for the right reason", as opposed to vacuously (see TACAS paper and papers on vacuity detection).
Proof maintenance: given a property similar to the one for which a proof exists, see which part of the proof can be reused.
Compositional verification: organizing verification so that a feature can be verified separately from the system and then composed (see FOAL paper)

Last updated: Sept. 3, 2003