Sciweavers

Share
PLDI
2009
ACM

An integrated proof language for imperative programs

9 years 7 months ago
An integrated proof language for imperative programs
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 lemm...
Karen Zee, Viktor Kuncak, Martin C. Rinard
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where PLDI
Authors Karen Zee, Viktor Kuncak, Martin C. Rinard
Comments (0)
books