Checking reachability using matching logic

Grigore Roşu, Andrei Ştefǎnescu

Research output: Contribution to journalArticlepeer-review

Abstract

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
Volume47
Issue number10
DOIs
StatePublished - Oct 1 2012

Keywords

  • 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