IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

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

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/28357

Files in this item

File Description Format
PDF rosu-stefanescu-2011-tr.pdf (285KB) main article PDF
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
Type: Text
Language: English
URI: http://hdl.handle.net/2142/28357
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2011-11-16
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 110
  • Downloads this Month: 1
  • Downloads Today: 0

Browse

My Account

Information

Access Key