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 ; Grigore Rosu - 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

Secondary volumes: Selected Papers of the 25th International Conference on Rewriting Techniques and Applications and the 12th International Conference on Typed Lambda Calculus and Applications (RTA and TLCA 2014)

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

36 Documents citing this article

Erik Voogd;Einar Broch Johnsen;Åsmund Aqissiaq Arild Kløvstad;Jurriaan Rot;Alexandra Silva, 2024, Correct and Complete Symbolic Execution for Free, UCL Discovery (University College London), pp. 237-255, 10.1007/978-3-031-76554-4_13, https://discovery.ucl.ac.uk/id/eprint/10203307/.

Misaki Kojima;Naoki Nishida, 2024, A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations, Journal of Information Processing, 32, 0, pp. 417-435, 10.2197/ipsjjip.32.417, http://dx.doi.org/10.2197/ipsjjip.32.417.

Misaki Kojima;Naoki Nishida, 2024, On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness, Lecture notes in computer science, pp. 54-70, 10.1007/978-3-031-72621-7_5.

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

Nico Naus;Freek Verbeek;Marc Schoolderman;Binoy Ravindran, 2023, Low-Level Reachability Analysis Based on Formal Logic, Lecture notes in computer science, pp. 21-39, 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, Electronic Proceedings in Theoretical Computer Science, 369, pp. 1-16, 10.4204/eptcs.369.1, https://doi.org/10.4204/eptcs.369.1.

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

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

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

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

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

Andrei Arusoaie;Dorel Lucanu, 2019, Unification in Matching Logic, arXiv (Cornell University), pp. 502-518, 10.1007/978-3-030-30942-8_30, http://export.arxiv.org/pdf/1811.02835.

Andrei-Sebastian Buruiană;Ştefan Ciobâcă, 2019, Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics, Electronic Proceedings in Theoretical Computer Science, 289, pp. 1-16, 10.4204/eptcs.289.1, https://doi.org/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, Electronic Proceedings in Theoretical Computer Science, 303, pp. 32-47, 10.4204/eptcs.303.3, https://doi.org/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, 2018, Symbolic Reasoning Methods in Rewriting Logic and Maude, Lecture notes in computer science, pp. 25-60, 10.1007/978-3-662-57669-4_2.

José Meseguer, 2018, Generalized Rewrite Theories and Coherence Completion, Lecture notes in computer science, pp. 164-183, 10.1007/978-3-319-99840-4_10.

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

Rakesh Bobba;Jon Grov;Indranil Gupta;Si Liu;José Meseguer;et al., 2018, Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude, Assured Cloud Computing, pp. 10-48, 10.1002/9781119428497.ch2.

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

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

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

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

Bartosz Zieliński, 2017, Modular Term-Rewriting Framework for Artifact-Centric Business Process Modelling, Lecture notes in computer science, pp. 71-78, 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, 2016, Semantics-based program verifiers for all languages, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 74-91, 10.1145/2983990.2984027.

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

Dániel Horpácsi;Judit Kőszegi;Simon Thompson, 2016, Towards Trustworthy Refactoring in Erlang, Electronic Proceedings in Theoretical Computer Science, 216, pp. 83-103, 10.4204/eptcs.216.5, https://doi.org/10.4204/eptcs.216.5.

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

Vlad Rusu;Andrei Arusoaie, 2016, Proving Reachability-Logic Formulas Incrementally, Lecture notes in computer science, pp. 134-151, 10.1007/978-3-319-44802-2_8.

Ştefan Ciobâcă;Dorel Lucanu;Vlad Rusu;Grigore Roşu, 2016, A language-independent proof system for full program equivalence, LillOA (Université de Lille (University Of Lille)), 28, 3, pp. 469-497, 10.1007/s00165-016-0361-7, http://hdl.handle.net/20.500.12210/25091.

Dorel Lucanu;Vlad Rusu;Andrei Arusoaie;David Nowak, 2015, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, LillOA (Université de Lille (University Of Lille)), pp. 451-474, 10.1007/978-3-319-23165-5_21, http://hdl.handle.net/20.500.12210/25548.

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

Ştefan Ciobâcă;Dorel Lucanu;Vlad Rusu;Grigore Roşu, 2015, A Theoretical Foundation for Programming Languages Aggregation, Lecture notes in computer science, pp. 30-47, 10.1007/978-3-319-28114-8_3.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3437 times.

This article's PDF has been downloaded 580 times.