Checking reachability using matching logic

Grigore Roşu; Andrei Ştefǎnescu

doi:10.1145/2398857.2384656

Checking reachability using matching logic

Grigore Roşu, Andrei Ştefǎnescu

Research output: Contribution to journal › Article › peer-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 language	English (US)
Pages (from-to)	555-574
Number of pages	20
Journal	ACM SIGPLAN Notices
Volume	47
Issue number	10
DOIs	https://doi.org/10.1145/2398857.2384656
State	Published - Oct 2012

Keywords

Hoare logic
Matching logic
Reachability

ASJC Scopus subject areas

General Computer Science

Online availability

10.1145/2398857.2384656

Library availability

Discover UIUC Full Text

Cite this

@article{5865282a18b74f23b9a080cf3832946a,

title = "Checking reachability using matching logic",

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.",

keywords = "Hoare logic, Matching logic, Reachability",

author = "Grigore Ro{\c s}u and Andrei {\c S}tefǎnescu",

year = "2012",

month = oct,

doi = "10.1145/2398857.2384656",

language = "English (US)",

volume = "47",

pages = "555--574",

journal = "ACM SIGPLAN Notices",

issn = "1523-2867",

publisher = "Association for Computing Machinery",

number = "10",

}

TY - JOUR

T1 - Checking reachability using matching logic

AU - Roşu, Grigore

AU - Ştefǎnescu, Andrei

PY - 2012/10

Y1 - 2012/10

N2 - 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.

AB - 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.

KW - Hoare logic

KW - Matching logic

KW - Reachability

UR - http://www.scopus.com/inward/record.url?scp=84870417831&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84870417831&partnerID=8YFLogxK

U2 - 10.1145/2398857.2384656

DO - 10.1145/2398857.2384656

M3 - Article

AN - SCOPUS:84870417831

SN - 1523-2867

VL - 47

SP - 555

EP - 574

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

IS - 10

ER -

Checking reachability using matching logic

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this