Andrei Stefanescu ; Stefan Ciobaca ; Radu Mereuta ; Brandon Moore ; Traian Florin Serbanuta et al. - All-Path Reachability Logic

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

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

    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 (

    Volume: Volume 15, Issue 2
    Published on: April 30, 2019
    Accepted 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
    Fundings :
      Source : OpenAIRE Research Graph
    • SHF: Small: Usable Verification using Rewriting and Matching Logic; Funder: National Science Foundation; Code: 1218605

    Linked data

    Source : ScholeXplorer HasVersion DOI 10.48550/arxiv.1810.10826
    • 10.48550/arxiv.1810.10826
    All-Path Reachability Logic
    Stefanescu, Andrei ; Ciobaca, Stefan ; Mereuta, Radu ; Moore, Brandon ; Serbanuta, Traian Florin ; Rosu, Grigore ;


    Consultation statistics

    This page has been seen 546 times.
    This article's PDF has been downloaded 270 times.