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

From Hoare Logic to Matching Logic

Show simple item record

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

Files in this item

File Description Format
PDF rosu-stefanescu-2012-fm-submission.pdf (166KB) (no description provided) PDF
Title: From Hoare Logic to Matching Logic
Author(s): Rosu, Grigore
Contributor(s): Stefanescu, Andrei
Subject(s): Hoare logic Matching logic Relative completeness Program verification
Abstract: Matching logic has been recently proposed as an alternative program verification approach. Unlike Hoare logic, where one defines a language-specific proof system that needs to be proved sound for each language separately, matching logic provides a language-independent and sound proof system that directly uses the trusted operational semantics of the language as axioms. Matching logic thus has a clear practical advantage: it eliminates the need for an additional semantics of the same language in order to reason about programs, and implicitly eliminates the need for tedious soundness proofs. What is not clear, however, is whether matching logic is as powerful as Hoare logic. This paper introduces a technique to mechanically translate Hoare logic proof derivations into equivalent matching logic proof derivations. The presented technique has two consequences: first, it suggests that matching logic has no theoretical limitation over Hoare logic; and second, it provides a new approach to prove Hoare logics sound.
Issue Date: 2012-03
Genre: Technical ReportArticle
Type: Text
Language: English
URI: http://hdl.handle.net/2142/30471
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2012-04-05
 

This item appears in the following Collection(s)

Show simple item record

Item Statistics

  • Total Downloads: 113
  • Downloads this Month: 2
  • Downloads Today: 0

Browse

My Account

Information

Access Key