An Integrated Proof Language for Imperative Programs

paper ps   
We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge generated proof obligations. It is designed to 1) enable developers to resolve key choice points in complex program correctness proofs, thereby enabling automated reasoning systems to successfully prove the desired correctness properties; 2) allow developers to identify key lemmas for the reasoning systems to prove, thereby guiding the reasoning systems to find an effective proof decomposition; 3) enable multiple reasoning systems to work together productively to prove a single correctness property by providing a mechanism that developers can use to divide the property into lemmas, each of which is suitable for a different reasoning system; and 4) enable developers to identify specific lemmas that the reasoning systems should use when attempting to prove other lemmas or correctness properties, thereby appropriately confining the search space so that the reasoning systems can find a proof in an acceptable amount of time. The language includes a rich set of declarative proof constructs that enables developers to direct the reasoning systems as little or as much as they desire. Because the declarative proof statements are embedded into the program as specialized comments, they also serve as verified documentation and are a natural extension of the assertion mechanism found in most program verification systems. We have implemented our integrated proof language in the context of a program verification system for Java and used the resulting system to verify a collection of linked data structure implementations. Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of automated reasoning systems.

Citation

Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2009.

BibTex Entry

@inproceedings{ZeeETAL09IntegratedProofLanguageforImperativePrograms,
  author = {Karen Zee and Viktor Kuncak and Martin Rinard},
  title = {An Integrated Proof Language for Imperative Programs},
  booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation  (PLDI)},
  year = 2009,
  abstract = {We present an integrated proof language for guiding the actions of
multiple reasoning systems as they work together to prove complex
correctness properties of imperative programs. The language operates
in the context of a program verification system that uses multiple
reasoning systems to discharge generated proof obligations.  It is
designed to 1) enable developers to resolve key choice points in
complex program correctness proofs, thereby enabling automated
reasoning systems to successfully prove the desired correctness
properties; 2) allow developers to identify key lemmas for the
reasoning systems to prove, thereby guiding the reasoning systems to
find an effective proof decomposition; 3) enable multiple reasoning
systems to work together productively to prove a single correctness
property by providing a mechanism that developers can use to divide
the property into lemmas, each of which is suitable for a different
reasoning system; and 4) enable developers to identify specific lemmas
that the reasoning systems should use when attempting to prove other
lemmas or correctness properties, thereby appropriately confining the
search space so that the reasoning systems can find a proof in an
acceptable amount of time.

The language includes a rich set of declarative proof constructs that
enables developers to direct the reasoning systems as little or as
much as they desire.  Because the declarative proof statements are
embedded into the program as specialized comments, they also serve as
verified documentation and are a natural extension of the assertion
mechanism found in most program verification systems.

We have implemented our integrated proof language in the context of a
program verification system for Java and used the resulting system to
verify a collection of linked data structure implementations.  Our
experience indicates that our proof language makes it possible to
successfully prove complex program correctness properties that are
otherwise beyond the reach of automated reasoning systems.
}
}