|Abstract:||Matching logic allows to specify structural properties about program
configurations by means of special formulae, called patterns, and to
reason about them by means of pattern matching.
This paper proposes rewriting over matching logic formulae, which generalizes
both term rewriting and Hoare triples, as a unified framework for operational
semantics and for program verification.
A programming language is formally defined as a set of rewrite rules. A
language-independent nine-rule proof system then can be used either to derive
any operational program behavior, or to verify programs against arbitrary
properties specified also as rewrite rules, thus reducing the gap between
operational semantics and axiomatic semantics to zero.
The proof system is proved both sound and complete for operational
semantics and partially correct for program verification.
All these proofs are language-independent.
A matching logic verifier for a
fragment of C, called MatchC, has been implemented and evaluated with
encouraging results on a series of non-trivial programs, attesting to the
practicality of the approach.