From Hoare logic to matching logic reachability

Grigore Roşu, Andrei Ştefǎnescu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationFM 2012
Subtitle of host publicationFormal Methods - 18th International Symposium, Proceedings
Number of pages16
StatePublished - 2012
Event18th International Symposium on Formal Methods, FM 2012 - Paris, France
Duration: Aug 27 2012Aug 31 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7436 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other18th International Symposium on Formal Methods, FM 2012

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'From Hoare logic to matching logic reachability'. Together they form a unique fingerprint.

Cite this