Stefanescu, Andrei and Ciobaca, Stefan and Mereuta, Radu and Moore, Brandon and Serbanuta, Traian Florinet al. - All-Path Reachability Logic

lmcs:4939 - Logical Methods in Computer Science, April 30, 2019, Volume 15, Issue 2
All-Path Reachability Logic

Authors: Stefanescu, Andrei and Ciobaca, Stefan and Mereuta, Radu and Moore, Brandon and Serbanuta, Traian Florin and Rosu, Grigore

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 in Coq. This approach is implemented in a tool for semantics-based verification as part of the K framework (http://kframework.org)


Source : oai:arXiv.org:1810.10826
Volume: Volume 15, Issue 2
Published on: April 30, 2019
Submitted on: October 31, 2018
Keywords: Computer Science - Programming Languages,Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science


Share