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.
This is the default collection for all research and scholarship developed by faculty, staff, or students at the University of Illinois at Urbana-Champaign
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
