The following pages link to One-Path Reachability Logic (Q5271073):
Displaying 24 items.
- A generic framework for symbolic execution: a coinductive approach (Q507361) (← links)
- A language-independent proof system for full program equivalence (Q510898) (← links)
- Language definitions as rewrite theories (Q730476) (← links)
- Finite-trace linear temporal logic: coinductive completeness (Q1667649) (← links)
- (Co)inductive proof systems for compositional proofs in reachability logic (Q1996855) (← links)
- On composition of bounded-recall plans (Q2046034) (← links)
- Non-well-founded deduction for induction and coinduction (Q2055840) (← links)
- Capturing constrained constructor patterns in matching logic (Q2096417) (← links)
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle (Q2119971) (← links)
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs (Q2163179) (← links)
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages (Q2237340) (← links)
- Using well-founded relations for proving operational termination (Q2303238) (← links)
- Program verification by coinduction (Q2324001) (← links)
- Executing and verifying higher-order functional-imperative programs in Maude (Q2409629) (← links)
- Proving Reachability-Logic Formulas Incrementally (Q2827839) (← links)
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Q2945720) (← links)
- From Rewriting Logic, to Programming Language Semantics, to Program Verification (Q2945730) (← links)
- Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework (Q4988925) (← links)
- All-Path Reachability Logic (Q5170834) (← links)
- Matching µ-logic: Foundation of K framework (Q5875341) (← links)
- Verification of the IBOS Browser Security Properties in Reachability Logic (Q6486045) (← links)
- Low-level reachability analysis based on formal logic (Q6535328) (← links)
- Unification in matching logic (Q6535966) (← links)
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems (Q6671788) (← links)
