One-path reachability logic
From MaRDI portal
Recommendations
Cited in
(32)- Finite-trace linear temporal logic: coinductive completeness
- A constructor-based reachability logic for rewrite theories
- (Co)inductive proof systems for compositional proofs in reachability logic
- On composition of bounded-recall plans
- Non-well-founded deduction for induction and coinduction
- Capturing constrained constructor patterns in matching logic
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
- Reasoning about iteration and recursion uniformly based on big-step semantics
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
- Using well-founded relations for proving operational termination
- Program verification by coinduction
- Executing and verifying higher-order functional-imperative programs in Maude
- Proving reachability-logic formulas incrementally
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
- From rewriting logic, to programming language semantics, to program verification
- Towards a unified theory of operational and axiomatic semantics
- From hoare logic to matching logic reachability
- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- A generic framework for symbolic execution: a coinductive approach
- A language-independent proof system for full program equivalence
- A constructor-based reachability logic for rewrite theories
- Matching µ-logic: Foundation of K framework
- Verification of the IBOS Browser Security Properties in Reachability Logic
- Low-level reachability analysis based on formal logic
- Unification in matching logic
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
- Compositional correctness and completeness for symbolic partial order reduction
- Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms
- Cartesian reachability logic: a language-parametric logic for verifying k-safety properties
- Language definitions as rewrite theories
- \( \mathbb{K}\) definitions as matching logic theories, formally
This page was built for publication: One-path reachability logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5271073)
