TY - GEN
T1 - Program verification by coinduction
AU - Moore, Brandon
AU - Peña, Lucas
AU - Rosu, Grigore
N1 - Publisher Copyright:
© The Author(s) 2018.
Copyright:
Copyright 2018 Elsevier B.V., All rights reserved.
PY - 2018
Y1 - 2018
N2 - We present a novel program verification approach based on coinduction, which takes as input an operational semantics. No intermediates like program logics 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.
AB - We present a novel program verification approach based on coinduction, which takes as input an operational semantics. No intermediates like program logics 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.
UR - http://www.scopus.com/inward/record.url?scp=85045635947&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85045635947&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-89884-1_21
DO - 10.1007/978-3-319-89884-1_21
M3 - Conference contribution
AN - SCOPUS:85045635947
SN - 9783319898834
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 589
EP - 618
BT - Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
A2 - Ahmed, Amal
PB - Springer
T2 - 27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Y2 - 14 April 2018 through 20 April 2018
ER -