Difference between revisions of "Semantics-Based Program Verifiers for All Languages"

From FSL
Jump to: navigation, search
Line 1: Line 1:
<private>== Submitted to POPL'16 ==
+
== Submitted to OOPSLA'16 ==
<pubbib id='stefanescu-park-yuwen-li-rosu-2016-popl-submission' template='PubDefaultWithAbstractAndTitle'/>
+
<pubbib id='stefanescu-park-yuwen-li-rosu-2016-oopsla' template='PubDefaultWithAbstractAndTitle'/>
 +
<private>== Submitted to OOPSLA'16 ==
 +
<pubbib id='stefanescu-park-yuwen-li-rosu-2016-oopsla-submission' template='PubDefaultWithAbstractAndTitle'/>
 
== Submitted to PLDI'16 ==
 
== Submitted to PLDI'16 ==
 
<pubbib id='stefanescu-park-yuwen-li-rosu-2016-pldi-submission' template='PubDefaultWithAbstractAndTitle'/>
 
<pubbib id='stefanescu-park-yuwen-li-rosu-2016-pldi-submission' template='PubDefaultWithAbstractAndTitle'/>
== Submitted to OOPSLA'16 ==
+
== Submitted to POPL'16 ==
<pubbib id='stefanescu-park-yuwen-li-rosu-2016-oopsla-submission' template='PubDefaultWithAbstractAndTitle'/></private>
+
<pubbib id='stefanescu-park-yuwen-li-rosu-2016-popl-submission' template='PubDefaultWithAbstractAndTitle'/></private>

Revision as of 16:14, 8 July 2016

Submitted to OOPSLA'16

Semantics-Based Program Verifiers for All Languages
Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
OOPSLA'16, ACM, pp 74-91. 2016
Abstract. We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound and relatively complete reachability logic proof system to prove the specifications using the semantics. We instantiate the framework with the semantics of one academic language, KernelC, as well as with three recent semantics of real-world languages, C, Java, and JavaScript, developed independently. We evaluate our approach empirically and show that the generated program verifiers can check automatically the full functional correctness of challenging heap-manipulating programs implementing operations on list and tree data structures, like AVL trees. This is the first approach that can turn the operational semantics of real-world languages into correct-by-construction automatic verifiers.
PDF, Slides(PDF), Matching Logic, DOI, OOPSLA'16, BIB


Personal tools
Namespaces

Variants
Actions
Navigation