Checking reachability using matching logic

Grigore Roşu, Andrei Ştefǎnescu

Research output: Contribution to journalArticlepeer-review


This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is languageindependent and consists of eight proof rules. The proof system is proved partially correct and relatively complete (with respect to the programming language configuration model). To show its practicality, the generic framework is instantiated with a fragment of C and evaluated with encouraging results.

Original languageEnglish (US)
Pages (from-to)555-574
Number of pages20
JournalACM SIGPLAN Notices
Issue number10
StatePublished - Oct 1 2012


  • Hoare logic
  • Matching logic
  • Reachability

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Checking reachability using matching logic'. Together they form a unique fingerprint.

Cite this