TY - GEN
T1 - All-path reachability logic
AU - Ştefǎnescu, Andrei
AU - Ciobâč, Ştefan
AU - Mereuta, Radu
AU - Moore, Brandon M.
AU - Şerbǎnutǎ, Traian Florin
AU - Roşu, Grigore
PY - 2014
Y1 - 2014
N2 - 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 framework.
AB - 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 framework.
UR - http://www.scopus.com/inward/record.url?scp=84958548820&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84958548820&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-08918-8_29
DO - 10.1007/978-3-319-08918-8_29
M3 - Conference contribution
AN - SCOPUS:84958548820
SN - 9783319089171
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 425
EP - 440
BT - Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PB - Springer
T2 - 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
Y2 - 14 July 2014 through 17 July 2014
ER -