All-Path Reachability Logic

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

doi:10.23638/LMCS-15(2:5)2019

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

Bibliographic References

32 Documents citing this article

Misaki Kojima;Naoki Nishida, Lecture notes in computer science, From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting, pp. 161-179, 2023, 10.1007/978-3-031-24841-2_11.

Nico Naus;Freek Verbeek;Marc Schoolderman;Binoy Ravindran, Lecture notes in computer science, Low-Level Reachability Analysis Based on Formal Logic, pp. 21-39, 2023, 10.1007/978-3-031-38828-6_2.

Zhengyao Lin;Xiaohong Chen;Minh-Thai Trinh;John Wang;Grigore Roşu, 2023, Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier, Proceedings of the ACM on Programming Languages, 7, OOPSLA1, pp. 56-84, 10.1145/3586029, https://doi.org/10.1145/3586029.

Andrei Arusoaie;Dorel Lucanu, 2022, Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification, arXiv (Cornell University), 369, pp. 1-16, 10.4204/eptcs.369.1.

Raúl López-Rueda;Santiago Escobar, Lecture notes in computer science, Canonical Narrowing for Variant-Based Conditional Rewrite Theories, pp. 20-35, 2022, 10.1007/978-3-031-17244-1_2.

Dominik Klumpp;Philip Lenzen, Lecture notes in computer science, $$\mathbb {K}$$ and KIV: Towards Deductive Verification for Arbitrary Programming Languages, pp. 98-119, 2021, 10.1007/978-3-030-73785-6_6.

Liron Cohen, Lecture notes in computer science, Non-well-founded Deduction for Induction and Coinduction, pp. 3-24, 2021, 10.1007/978-3-030-79876-5_1, https://doi.org/10.1007/978-3-030-79876-5_1.

Liyi Li;Elsa L. Gunter, Lecture notes in computer science, A Complete Semantics of $$\mathbb {K}$$ and Its Translation to Isabelle, pp. 152-171, 2021, 10.1007/978-3-030-85315-0_10.

Stephen Skeirik;José Meseguer;Camilo Rocha, arXiv (Cornell University), Verification of the IBOS Browser Security Properties in Reachability Logic, pp. 176-196, 2020, 10.1007/978-3-030-63595-4_10, https://arxiv.org/abs/2005.12232.

Andrei Arusoaie;Dorel Lucanu, Lecture notes in computer science, Unification in Matching Logic, pp. 502-518, 2019, 10.1007/978-3-030-30942-8_30.

Andrei-Sebastian Buruiană;Ştefan Ciobâcă, 2019, Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics, arXiv (Cornell University), 289, pp. 1-16, 10.4204/eptcs.289.1.

Francisco Durán;Steven Eker;Santiago Escobar;Narciso Martí-Oliet;José Meseguer;et al., 2019, Programming and symbolic computation in Maude, Journal of Logical and Algebraic Methods in Programming, 110, pp. 100497, 10.1016/j.jlamp.2019.100497, https://doi.org/10.1016/j.jlamp.2019.100497.

Vlad Rusu;David Nowak, 2019, (Co)inductive Proof Systems for Compositional Proofs in Reachability Logic, arXiv (Cornell University), 303, pp. 32-47, 10.4204/eptcs.303.3.

Grigore Roşu, 2018, Finite-trace linear temporal logic: coinductive completeness, Formal Methods in System Design, 53, 1, pp. 138-163, 10.1007/s10703-018-0321-3.

José Meseguer, IDEALS (University of Illinois Urbana-Champaign), Generalized Rewrite Theories and Coherence Completion, pp. 164-183, 2018, 10.1007/978-3-319-99840-4_10, http://hdl.handle.net/2142/99546.

José Meseguer, Lecture notes in computer science, Symbolic Reasoning Methods in Rewriting Logic and Maude, pp. 25-60, 2018, 10.1007/978-3-662-57669-4_2.

Liyi Li;Elsa L. Gunter, Lecture notes in computer science, IsaK-Static: A Complete Static Semantics of $$\mathbb {K}$$ , pp. 196-215, 2018, 10.1007/978-3-030-02146-7_10.

Stephen Skeirik;Andrei Stefanescu;José Meseguer, arXiv (Cornell University), A Constructor-Based Reachability Logic for Rewrite Theories, pp. 201-217, 2018, 10.1007/978-3-319-94460-9_12, https://arxiv.org/abs/1709.05045.

Xiaohong Chen;Grigore Roşu, Lecture notes in computer science, A Language-Independent Program Verification Framework, pp. 92-102, 2018, 10.1007/978-3-030-03421-4_7.

Ştefan Ciobâcă;Andrei Arusoaie;Dorel Lucanu, Lecture notes in computer science, Unification Modulo Builtins, pp. 179-195, 2018, 10.1007/978-3-662-57669-4_10.

Ştefan Ciobâcă;Dorel Lucanu, arXiv (Cornell University), A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems, pp. 295-311, 2018, 10.1007/978-3-319-94205-6_20, http://arxiv.org/abs/1804.08308.

Bartosz Zieliński, Lecture notes in computer science, Modular Term-Rewriting Framework for Artifact-Centric Business Process Modelling, pp. 71-78, 2017, 10.1007/978-3-319-66854-3_6.

Andrei Stefănescu;Daejun Park;Shijiao Yuwen;Yilong Li;Grigore Roşu, 2016, Semantics-based program verifiers for all languages, ACM SIGPLAN Notices, 51, 10, pp. 74-91, 10.1145/3022671.2984027, https://doi.org/10.1145/3022671.2984027.

Andrei Stefănescu;Daejun Park;Shijiao Yuwen;Yilong Li;Grigore Roşu, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Semantics-based program verifiers for all languages, 2016, Amsterdam Netherlands, 10.1145/2983990.2984027.

Dorel Lucanu;Traian-Florin Şerbănuţă;Grigore Roşu, Lecture notes in computer science, Towards a $$\mathbb {K}$$ool Future, pp. 325-343, 2016, 10.1007/978-3-319-30734-3_22.

Dániel Horpácsi;Judit Kőszegi;Simon Thompson, 2016, Towards Trustworthy Refactoring in Erlang, arXiv (Cornell University), 216, pp. 83-103, 10.4204/eptcs.216.5.

Grigore Roşu, Lecture notes in computer science, Finite-Trace Linear Temporal Logic: Coinductive Completeness, pp. 333-350, 2016, 10.1007/978-3-319-46982-9_21.

Vlad Rusu;Andrei Arusoaie, Proving Reachability-Logic Formulas Incrementally, pp. 134-151, 2016, 10.1007/978-3-319-44802-2_8, https://hal.inria.fr/hal-01282379.

Ştefan Ciobâcă;Dorel Lucanu;Vlad Rusu;Grigore Roşu, 2016, A language-independent proof system for full program equivalence, 28, 3, pp. 469-497, 10.1007/s00165-016-0361-7, https://hal.inria.fr/hal-01245528.

Dorel Lucanu;Vlad Rusu;Andrei Arusoaie;David Nowak, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, pp. 451-474, 2015, 10.1007/978-3-319-23165-5_21, https://hal.inria.fr/hal-01158941.

Grigore Roșu, Lecture notes in computer science, From Rewriting Logic, to Programming Language Semantics, to Program Verification, pp. 598-616, 2015, 10.1007/978-3-319-23165-5_28.

Ştefan Ciobâcă;Dorel Lucanu;Vlad Rusu;Grigore Roşu, A Theoretical Foundation for Programming Languages Aggregation, pp. 30-47, 2015, 10.1007/978-3-319-28114-8_3, https://hal.inria.fr/hal-01076641.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1864 times.

This article's PDF has been downloaded 402 times.