Difference between revisions of "From Hoare Logic to Matching Logic Reachability"
From FSL
| Line 1: | Line 1: | ||
== FM'12 == | == FM'12 == | ||
| − | < | + | <pubbib id='rosu-stefanescu-2012-fm' template='PubDefaultWithAbstractAndTitle'/> |
== Submitted to FM'12 == | == Submitted to FM'12 == | ||
<pub id='rosu-stefanescu-2012-fm-submission' template='PubDefaultWithAbstractAndTitle'/></private> | <pub id='rosu-stefanescu-2012-fm-submission' template='PubDefaultWithAbstractAndTitle'/></private> | ||
Revision as of 04:04, 25 February 2016
FM'12
- From Hoare Logic to Matching Logic Reachability
- Grigore Rosu and Andrei Stefanescu
- FM'12, LNCS 7436, pp 387-402. 2012
- Abstract. Matching logic reachability 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 reachability provides a *language-independent* and *sound* proof system that directly uses the trusted operational semantics of the language as axioms. Matching logic reachability 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 reachability is as powerful as Hoare logic. This paper introduces a technique to mechanically translate Hoare logic proof derivations into equivalent matching logic reachability proof derivations. The presented technique has two consequences: first, it suggests that matching logic reachability has no theoretical limitation over Hoare logic; and second, it provides a new approach to prove Hoare logics sound.
Submitted to FM'12
</private>
Technical Reports
- From Hoare Logic to Matching Logic Reachability
- Grigore Rosu and Andrei Stefanescu
- Technical Report http://hdl.handle.net/2142/31335, June 2012
- Abstract. Matching logic reachability 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 reachability provides a *language-independent* and *sound* proof system that directly uses the trusted operational semantics of the language as axioms. Matching logic reachability 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 reachability is as powerful as Hoare logic. This paper introduces a technique to mechanically translate Hoare logic proof derivations into equivalent matching logic reachability proof derivations. The presented technique has two consequences: first, it suggests that matching logic reachability has no theoretical limitation over Hoare logic; and second, it provides a new approach to prove Hoare logics sound.
- PDF, Matching Logic, TR@UIUC, , BIB
