Difference between revisions of "Reachability Logic in K"

From FSL
Jump to: navigation, search
Line 3: Line 3:
 
<private>== Submitted to RTA'14 ==
 
<private>== Submitted to RTA'14 ==
 
<pubbib id='stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta-submission' template='PubDefaultWithAbstractAndTitle'/></private>
 
<pubbib id='stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta-submission' template='PubDefaultWithAbstractAndTitle'/></private>
 +
<pubbib id='stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta' template='PubDefaultWithAbstractAndTitle'/>
 
== Technical Report ==
 
== Technical Report ==
 
<pubbib id='stefanescu-ciobaca-moore-serbanuta-rosu-2013-tr' template='PubDefaultWithAbstractAndTitle'/>
 
<pubbib id='stefanescu-ciobaca-moore-serbanuta-rosu-2013-tr' template='PubDefaultWithAbstractAndTitle'/>

Revision as of 02:21, 2 May 2014


All-Path Reachability Logic
Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
RTA'14, LNCS 8560, pp 425-440. 2014
Abstract. This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g. concurrent) languages, referred to as *all-path reachability logic*. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized (Coq). This approach is implemented in a tool for semantics-based verification as part of the K framework.
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB

Technical Report

Personal tools
Namespaces

Variants
Actions
Navigation