Checking reachability using matching logic ?

Grigore Rosu, Andrei Stefanescu

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

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)
Title of host publicationSPLASH 2012
Subtitle of host publicationOOPSLA'12 - Proceedings of the 2012 ACM International Conference on Object Oriented Programming SystemsLanguages and Applications
Pages555-574
Number of pages20
DOIs
StatePublished - Nov 27 2012
Event2012 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012 - Tucson, AZ, United States
Duration: Oct 19 2012Oct 26 2012

Publication series

NameProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA

Other

Other2012 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012
CountryUnited States
CityTucson, AZ
Period10/19/1210/26/12

Keywords

  • Hoare logic
  • Matching logic
  • Reachability

ASJC Scopus subject areas

  • Software

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

Cite this