Removing algebraic data types from constrained Horn clauses using difference predicates
From MaRDI portal
Publication:2096439
DOI10.1007/978-3-030-51074-9_6OpenAlexW3100001578MaRDI QIDQ2096439
Maurizio Proietti, Emanuele De Angelis, Alberto Pettorossi, Fabio Fioravanti
Publication date: 9 November 2022
Full work available at URL: https://arxiv.org/abs/2004.07749
Related Items (4)
Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Transformations of CLP modules
- Isabelle/HOL. A proof assistant for higher-order logic
- Relational verification through Horn clause transformation
- Reasoning about algebraic data types with abstractions
- Productive use of failure in inductive proof
- Automating induction for solving Horn clauses
- Generalized Property Directed Reachability
- Automating Induction with an SMT Solver
- Zeno: An Automated Prover for Properties of Recursive Data Structures
- Horn Clause Solvers for Program Verification
- Satisfiability Modulo Theories
- On Inductive and Coinductive Proofs via Unfold/Fold Transformations
- Solving Horn Clauses on Inductive Data Types Without Induction
- Automating Inductive Proofs Using Theory Exploration
- Induction for SMT Solvers
- Generalization strategies for the verification of infinite state systems
- The MathSAT5 SMT Solver
- Program Development in Computational Logic
- Case-Analysis for Rippling and Inductive Proof
This page was built for publication: Removing algebraic data types from constrained Horn clauses using difference predicates
