Program Verification by Coinduction

From FSL
Jump to: navigation, search

ESOP 2018

Program Verification by Coinduction
Brandon Moore and Lucas Pena and Grigore Rosu
ESOP'18, Springer, pp 589-618. 2018
Abstract. We present a novel program verification approach based on coinduction, which takes as input an operational semantics. No intermediates like axiomatic semantics or verification condition generators are needed. Specifications can be written using any state predicates. We implement our approach in Coq, giving a certifying language-independent verification framework. Our proof system is implemented as a single module imported unchanged into language-specific proofs. Automation is reached by instantiating a generic heuristic with language-specific tactics. Manual assistance is also smoothly allowed at points the automation cannot handle. We demonstrate the power and versatility of our approach by verifying algorithms as complicated as Schorr-Waite graph marking and instantiating our framework for object languages in several styles of semantics. Finally, we show that our coinductive approach subsumes reachability logic, a recent language-independent sound and (relatively) complete logic for program verification that has been instantiated with operational semantics of languages as complex as C, Java and JavaScript.
PDF, Matching Logic, DOI, ESOP'18, BIB

2015 Technical report

Program Verification by Coinduction
Brandon Moore and Grigore Rosu
Technical Report http://hdl.handle.net/2142/73177, February 2015
Abstract. We present a program verification framework based on coinduction, which makes it feasible to verify programs directly against an operational semantics, without requiring intermediates like axiomatic semantics or verification condition generators. Specifications can be written and proved using any predicates on the state space of the operational semantics. We implement our approach in Coq, giving a certifying language-independent verification framework. The core proof system is implemented as a single module imported unchanged into proofs of programs in any semantics. A comfortable level of automation is provided by instantiating a simple heuristic with tactics for language-specific tasks such as finding the successor of a symbolic state, and for domain-specific reasoning about the predicates used in a particular specification. This approach also smoothly allows manual assistance at points the automation cannot handle. We demonstrate the power of our approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the versatility by instantiating it for object languages in several styles of semantics. Despite the greater flexibility and generality of our approach, proof size and proof/certificate-checking time compare favorably with Bedrock, another Coq-based certifying program verification framework.
PDF, Matching Logic, DOI, BIB


Personal tools
Namespaces

Variants
Actions
Navigation