One-Path Reachability Logic
From MaRDI portal
Publication:5271073
DOI10.1109/LICS.2013.42zbMath1366.68182OpenAlexW2000387514MaRDI QIDQ5271073
Ştefan Ciobâcă, Andrei Ştefănescu, Brandon Moore, Grigore Roşu
Publication date: 3 July 2017
Published in: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1109/lics.2013.42
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
A complete semantics of \(\mathbb{K}\) and its translation to Isabelle, On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs, Finite-trace linear temporal logic: coinductive completeness, Executing and verifying higher-order functional-imperative programs in Maude, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, From Rewriting Logic, to Programming Language Semantics, to Program Verification, Matching µ-logic: Foundation of K framework, \( \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, Language definitions as rewrite theories, On composition of bounded-recall plans, Using well-founded relations for proving operational termination, 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
