We present a program-verification approach based on coinduction, which makes it feasible to verify programs given an operational semantics of a programming language, without constructing intermediates like axiomatic semantics or verification-condition generators. Specifications can be written using any state predicates.The key observations are that being able to define the correctness of a style of program specification as a greatest fixpoint means coinduction can be used to conclude that a specification holds, and that the number of cases that need to be enumerated to have a coinductively provable specification can be reduced to a feasible number by using a generalized coinduction principle (based on notions of ``coinduction up to'' developed for proving bisimulation) instead of the simplest statement of coinduction.We implement our approach in Coq, producing a certifying language-independent verification framework. The soundness of the system is based on a single module proving the necessary coinduction theorem, which is imported unchanged to prove programs in any language.We demonstrate the power of this approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the flexibility by instantiating it for language definitions covering several paradigms, and in several styles of semantics.We also demonstrate a comfortable level of proof automation for several languages and domains, using a common overall heuristic strategy instantiated with customized subroutines. Manual assistance is also smoothly integrated where automation is not completely successful.
PDF
download
878987797
028-85220240
