Removing algebraic data types from constrained Horn clauses using difference predicates
type: Item
instance of: scholarly article
title: Removing algebraic data types from constrained Horn clauses using difference predicates
DOI: 10.1007/978-3-030-51074-9_6
author: Emanuele De Angelis
author: Fabio Fioravanti
author: Alberto Pettorossi
author: Maurizio Proietti
publication date: 2022-11-09T00:00:00Z
full work available at URL: https://arxiv.org/abs/2004.07749
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7614508
describes a project that uses: Isabelle/HOL
describes a project that uses: Dafny
describes a project that uses: RAHFT
describes a project that uses: ProB
describes a project that uses: Spacer
describes a project that uses: Zeno
describes a project that uses: HipSpec
describes a project that uses: VeriMAP
describes a project that uses: CVC4
describes a project that uses: z3
describes a project that uses: IsaPlanner
describes a project that uses: PVS
describes a project that uses: OCaml
describes a project that uses: MathSAT5
MaRDI profile type: Publication
OpenAlex ID: W3100001578
cites work: Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
cites work: Satisfiability Modulo Theories
cites work: Horn Clause Solvers for Program Verification
cites work: The automation of proof by mathematical induction
cites work: The MathSAT5 SMT Solver
cites work: Automating Inductive Proofs Using Theory Exploration
cites work: Relational verification through Horn clause transformation
cites work: Solving Horn Clauses on Inductive Data Types Without Induction
cites work: Q5016384
cites work: Q4052071
cites work: Transformations of CLP modules
cites work: Program Development in Computational Logic
cites work: Generalization strategies for the verification of infinite state systems
cites work: Generalized Property Directed Reachability
cites work: Productive use of failure in inductive proof
cites work: Case-Analysis for Rippling and Inductive Proof
cites work: Automating Induction with an SMT Solver
cites work: Q3992908
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Reasoning about algebraic data types with abstractions
cites work: Induction for SMT Solvers
cites work: On Inductive and Coinductive Proofs via Unfold/Fold Transformations
cites work: Zeno: An Automated Prover for Properties of Recursive Data Structures
cites work: Automating induction for solving Horn clauses
description: scientific article; zbMATH DE number 7614508