Difference between revisions of "Checking Reachability using Matching Logic"
From FSL
| Line 1: | Line 1: | ||
== OOPSLA'12 == | == OOPSLA'12 == | ||
| − | < | + | <pubbib id='rosu-stefanescu-2012-oopsla' template='PubDefaultWithAbstractAndTitle'/> |
== Submitted to SPLASH'12 == | == Submitted to SPLASH'12 == | ||
<pub id='rosu-stefanescu-2012-splash-submission' template='PubDefaultWithAbstractAndTitle'/></private> | <pub id='rosu-stefanescu-2012-splash-submission' template='PubDefaultWithAbstractAndTitle'/></private> | ||
Revision as of 19:52, 25 February 2016
OOPSLA'12
- Checking Reachability using Matching Logic
- Grigore Rosu and Andrei Stefanescu
- OOPSLA'12, ACM, pp 555-574. 2012
- 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.
Submitted to SPLASH'12
</private>
Technical Report
- Checking Reachability using Matching Logic
- Grigore Rosu and Andrei Stefanescu
- Technical Report http://hdl.handle.net/2142/33771, August 2012
- 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.
