| Year | 2012 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Grigore Rosu, Andrei Stefanescu |
Links
Abstract
This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is language-independent 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.
BibTeX
@inproceedings{rosu-stefanescu-2012-oopsla,
author = {Grigore Rosu and Andrei Stefanescu},
title = {Checking Reachability using Matching Logic},
booktitle = {Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12)},
pages = {555-574},
year = {2012},
publisher = {ACM},
url_publisher = {http://doi.acm.org/10.1145/2384616.2384656},
url = {http://fsl.cs.illinois.edu/index.php/Checking_Reachability_using_Matching_Logic [See it on FSL-UIUC web page]}
}