All-Path Reachability Logic

DOI10.1007/978-3-319-08918-8_29zbMath1416.68052arXiv1810.10826OpenAlexW2259551671MaRDI QIDQ5170834

Andrei Ştefănescu, Brandon Moore, Ştefan Ciobâcă, Traian-Florin Şerbănuţă, Radu Mereuta, Grigore Roşu

Publication date: 24 July 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1810.10826

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle, Finite-trace linear temporal logic: coinductive completeness, Executing and verifying higher-order functional-imperative programs in Maude, Metalevel algorithms for variant satisfiability, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, From Rewriting Logic, to Programming Language Semantics, to Program Verification, Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting, A matching logic foundation for Alk, \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages, A generic framework for symbolic execution: a coinductive approach, A language-independent proof system for full program equivalence, (Co)inductive proof systems for compositional proofs in reachability logic, All-Path Reachability Logic, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, Non-well-founded deduction for induction and coinduction, Proving Reachability-Logic Formulas Incrementally, Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework, Capturing constrained constructor patterns in matching logic

Uses Software

• Coq
• z3
• Toolchain
• K tool
• PLT Redex
• K Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resources, concurrency, and local reasoning
• An overview of the K semantic framework
• The chemical abstract machine
• Winskel is (almost) right: Towards a mechanized semantics textbook
• A constructor-based reachability logic for rewrite theories
• Weakest pre-condition reasoning for Java programs with JML annotations
• A Dynamic Logic for Every Season
• Syntactic control of interference for separation logic
• Rewriting Modulo SMT and Open System Analysis
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Verified Software Toolchain
• Matching Logic: An Alternative to Hoare/Floyd Logic
• Granularity and Concurrent Separation Logic
• Proving Safety Properties of Rewrite Theories
• Towards a Unified Theory of Operational and Axiomatic Semantics
• A Marriage of Rely/Guarantee and Separation Logic
• Verifying properties of parallel programs
• Matching Logic
• From Hoare Logic to Matching Logic Reachability
• All-Path Reachability Logic
• Local rely-guarantee reasoning
• One-Path Reachability Logic
• Matching Logic - Extended Abstract (Invited Talk)
• An operational semantics for Scheme
• An axiomatic basis for computer programming