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