Towards a Unified Theory of Operational and Axiomatic Semantics — Extended Abstract
Rosu, Grigore
Loading…
Permalink
https://hdl.handle.net/2142/30472
Description
Title
Towards a Unified Theory of Operational and Axiomatic Semantics — Extended Abstract
Author(s)
Rosu, Grigore
Contributor(s)
Stefanescu, Andrei
Issue Date
2012-02
Keyword(s)
Operational semantics
Hoare logic
Partial correctness
Rewriting
Abstract
This paper presents a nine-rule language-independent
proof system that takes an operational semantics as axioms and derives program
properties, including ones corresponding to Hoare triples. This eliminates the
need for language-specific Hoare-style proof rules in order to verify programs,
and, implicitly, the tedious step of proving such proof rules sound for each
language separately. The key proof rule is Circularity, which is
coinductive in nature and allows for reasoning about constructs with repetitive
behaviors (e.g., loops). The generic proof system is shown sound and has been
implemented in the MatchC program verifier.
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.