Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework

Rosu, Grigore

Permalink

https://hdl.handle.net/2142/28357 Copy

Description

Title

Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework

Author(s)

Rosu, Grigore

Contributor(s)

Stefanescu, Andrei

Issue Date

2011-11-16

Keyword(s)

Matching logic, operational semantics, axiomatic semantics, term rewriting

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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/28357

Owning Collections