@inproceedings{stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta,
author = {Andrei \c{S}tef\u{a}nescu and \c{S}tefan Ciob\^{a}c\u{a} and
Radu Mereu\c{t}\u{a} and Brandon M. Moore and
Traian Florin \c{S}erb\u{a}nu\c{t}\u{a} and Grigore Ro\c{s}u},
title = {All-Path Reachability Logic},
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.
},
booktitle = {Proceedings of the Joint 25th International Conference on
Rewriting Techniques and Applications and 12th International
Conference on Typed Lambda Calculi and Applications
(RTA-TLCA'14)},
pages = {425-440},
month = {July},
year = {2014},
series = {LNCS},
volume = {8560},
publisher = {Springer},
author_id = {Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and
Brandon Moore and Traian Florin Serbanuta and
Grigore Rosu},
category = {fsl, executable_semantics, logics, matching_logic,
program_verification, programming_languages},
project_url = {http://matching-logic.org/},
project_name = {Matching Logic},
booktitle_acronym = {RTA'14},
booktitle_url = {http://vsl2014.at/pages/RTATLCA-cfp.html},
doi = {http://dx.doi.org/10.1007/978-3-319-08918-8_29},
presentation = {2014-07-16-RTA},
}