Automating induction for solving Horn clauses

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

Mathematics Subject Classification ID

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