TY - GEN
T1 - From Hoare logic to matching logic reachability
AU - Roşu, Grigore
AU - Ştefǎnescu, Andrei
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84866000815&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84866000815&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-32759-9_32
DO - 10.1007/978-3-642-32759-9_32
M3 - Conference contribution
AN - SCOPUS:84866000815
SN - 9783642327582
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 387
EP - 402
BT - FM 2012
T2 - 18th International Symposium on Formal Methods, FM 2012
Y2 - 27 August 2012 through 31 August 2012
ER -