Solving constrained Horn clauses over algebraic data types

DOI10.1007/978-3-031-24950-1_16MaRDI QIDQ6174408zbMATH OpenOpenAlexFDO

Authors Lucas Zavalía, Lidiia Chernigovskaia, Grigory Fedyukovich

Publication date 17 August 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-24950-1_16

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach
• Solving Horn clauses on inductive data types without induction
• Solving constrained Horn clauses using dependence-disjoint expansions
• Automating induction for solving Horn clauses

Cites work

• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• A decision procedure for (co)datatypes in SMT solvers
• An abstract decision procedure for a theory of inductive data types.
• Automated Reasoning
• Automating induction for solving Horn clauses
• Bridging arrays and ADTs in recursive proofs
• Combining forward and backward abstract interpretation of Horn clauses
• Decision procedures for algebraic data types with abstractions
• Global guidance for local generalization in model checking
• HoIce: an ICE-based non-linear Horn clause solver
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 7364138 (Why is no real title available?)
• scientific article; zbMATH DE number 7440190 (Why is no real title available?)
• scientific article; zbMATH DE number 7444022 (Why is no real title available?)
• ICE-based refinement type discovery for higher-order functional programs
• Induction for SMT solvers
• Inferring simple solutions to recursion-free Horn clauses via sampling
• Productive use of failure in inductive proof
• Quantified Heap Invariants for Object-Oriented Programs
• Reasoning about algebraic data types with abstractions
• Reasoning About Recursively Defined Data Structures
• Recursive data structures
• RustHorn: CHC-based verification for Rust programs
• SAT-Based Model Checking without Unrolling
• Solving Horn clauses on inductive data types without induction
• Solving non-linear Horn clauses using a linear Horn clause solver
• Synchronizing constrained Horn clauses

Cited in

(5)

• On a generalization of Horn constraint systems
• Solving constrained Horn clauses using dependence-disjoint expansions
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
• Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach
• The \textsc{Golem} Horn solver

This page was built for publication: Solving constrained Horn clauses over algebraic data types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174408)