Files in this item



application/pdfrosu-stefanescu-2011-tr.pdf (285kB)
main articlePDF


Title:Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework
Author(s):Rosu, Grigore
Contributor(s):Stefanescu, Andrei
Subject(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.
Issue Date:2011-11-16
Genre:Technical Report
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2011-11-16

This item appears in the following Collection(s)

Item Statistics