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 - https://doi.org/10.23638/LMCS-15(2:5)2019
All-Path Reachability LogicArticle

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 (http://kframework.org)

    https://doi.org/10.23638/LMCS-15(2:5)2019
    Source: arXiv.org:1810.10826
    Volume: Volume 15, Issue 2
    Published on: April 30, 2019
    Accepted on: November 20, 2018
    Submitted on: October 31, 2018
    Keywords: Computer Science - Programming Languages,Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science
    Licence: Attribution 4.0 International (CC BY 4.0)
    Funding:
      Source : OpenAIRE Graph
    • SHF: Small: Usable Verification using Rewriting and Matching Logic; Funder: National Science Foundation; Code: 1218605

    Publications

    HasVersion
    All-Path Reachability Logic
    • 1 ScholeXplorer

    References

    Share and export

    Consultation statistics

    This page has been seen 1074 times.
    This article's PDF has been downloaded 318 times.