| Year | 2014 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon Moore, Traian Serbanuta, Grigore Rosu |
Links
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.
BibTeX
@Proceedings{asda,
author = {A. Stefanescu and S. Ciobaca and R. Mereuta and B. M. Moore and Traian-Florin Serbanuta and Grigore Rosu},
title = {All-Path Reachability Logic},
booktitle = {Rewriting and Typed Lambda Calculi - Joint International Conference,
{RTA-TLCA} 2014, Held as Part of the Vienna Summer of Logic, {VSL}
2014, Vienna, Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
pages = {425--440},
year = {2014},
volume = {8560},
number = {},
publisher = {Springer},
url_publisher = {},
note = {},
url = {http://fsl.cs.illinois.edu/FSL/papers/2014/stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta/stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta-public.pdf[PDF]}
}