Automating induction for solving Horn clauses
From MaRDI portal
Publication:2164260
DOI10.1007/978-3-319-63390-9_30zbMath1494.68064arXiv1610.06768OpenAlexW2545358040MaRDI QIDQ2164260
Hiroki Sakamoto, Hiroshi Unno, Sho Torii
Publication date: 12 August 2022
Full work available at URL: https://arxiv.org/abs/1610.06768
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (17)
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ Constraint-based relational verification ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Loop verification with invariants and contracts ⋮ Asynchronous unfold/fold transformation for fixpoint logic ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Unbounded procedure summaries from bounded environments ⋮ Fold/Unfold Transformations for Fixpoint Logic ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Relational cost analysis in a functional-imperative setting
This page was built for publication: Automating induction for solving Horn clauses