Solving Horn Clauses on Inductive Data Types Without Induction

DOI10.1017/S1471068418000157zbMath1451.68172arXiv1804.09007MaRDI QIDQ4559806

Alberto Pettorossi, Emanuele De Angelis, Maurizio Proietti, Fabio Fioravanti

Publication date: 4 December 2018

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1804.09007

zbMATH Keywords

program transformationconstraint logic programmingprogram verificationconstrained Horn clausesinductively defined data types

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)

Related Items (13)

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Asynchronous unfold/fold transformation for fixpoint logic ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Fold/Unfold Transformations for Fixpoint Logic ⋮ Solving Horn Clauses on Inductive Data Types Without Induction – ERRATUM ⋮ ICE-based refinement type discovery for higher-order functional programs ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates

Uses Software

• ECCE
• z3
• PPL

Cites Work

• Unnamed Item
• Transformations of CLP modules
• Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
• Deforestation: Transforming programs to eliminate trees
• Horn Clause Solvers for Program Verification
• Program Verification using Constraint Handling Rules and Array Constraint Generalizations*
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Conjunctive partial deduction: foundations, control, algorithms, and experiments

This page was built for publication: Solving Horn Clauses on Inductive Data Types Without Induction