Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Abstract elided by the publisher.
Related papers
- Solving constrained Horn clauses modulo algebraic data types and recursive functions POPL 2022
- Solving Constrained Horn Clauses over Algebraic Data Types VMCAI 2023
- Automating Induction for Solving Horn Clauses CAV 2017
- Higher-order constrained horn clauses for verification POPL 2018
- Fast Approximations of Quantifier Elimination CAV 2023
- sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses CAV 2025
- Verification of Programs with ADTs Using Shallow Horn Clauses SAS 2024
- Program Verification with Constrained Horn Clauses (Invited Paper) CAV 2022