Solving constrained Horn clauses over algebraic data types

DOI10.1007/978-3-031-24950-1_16zbMath1529.68167OpenAlexW4316662769MaRDI QIDQ6174408

Lucas Zavalía, Grigory Fedyukovich, Lidiia Chernigovskaia

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)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about algebraic data types with abstractions
• Productive use of failure in inductive proof
• Automating induction for solving Horn clauses
• Global guidance for local generalization in model checking
• Bridging arrays and ADTs in recursive proofs
• A decision procedure for (co)datatypes in SMT solvers
• SAT-Based Model Checking without Unrolling
• Reasoning About Recursively Defined Data Structures
• Recursive data structures
• Solving Horn Clauses on Inductive Data Types Without Induction
• Synchronizing Constrained Horn Clauses
• Quantified Heap Invariants for Object-Oriented Programs
• RustHorn: CHC-Based Verification for Rust Programs
• Induction for SMT Solvers
• Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling
• Combining Forward and Backward Abstract Interpretation of Horn Clauses
• Decision procedures for algebraic data types with abstractions
• Automated Reasoning
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• ICE-based refinement type discovery for higher-order functional programs
• HoIce: an ICE-based non-linear Horn clause solver