Checking Reachability using Matching Logic

From FSL
Revision as of 03:39, 28 February 2013 by Stefane1 (Talk | contribs)

Jump to: navigation, search

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.
PDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB

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.
PDF, Matching Logic, TR@UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation