Removing algebraic data types from constrained Horn clauses using difference predicates

DOI10.1007/978-3-030-51074-9_6MaRDI QIDQ2096439zbMATH OpenOpenAlexFDO

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

Publication date 9 November 2022

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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Automating induction for solving Horn clauses
• Automating Induction with an SMT Solver
• Automating Inductive Proofs Using Theory Exploration
• Case-analysis for rippling and inductive proof
• Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
• Generalization strategies for the verification of infinite state systems
• Generalized property directed reachability
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 7444023 (Why is no real title available?)
• Induction for SMT solvers
• Isabelle/HOL. A proof assistant for higher-order logic
• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• Productive use of failure in inductive proof
• Program Development in Computational Logic
• Reasoning about algebraic data types with abstractions
• Relational verification through Horn clause transformation
• Satisfiability modulo theories
• Solving Horn clauses on inductive data types without induction
• The automation of proof by mathematical induction
• The MathSAT5 SMT solver
• Transformations of CLP modules
• Zeno: an automated prover for properties of recursive data structures

Cited in

(5)

• Symbolic automatic relations and their applications to SMT and CHC solving
• scientific article; zbMATH DE number 7453193 (Why is no real title available?)
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• scientific article; zbMATH DE number 7806141 (Why is no real title available?)
• An overview of the HFL model checking project

Describes a project that uses

Uses Software

• Isabelle/HOL
• Dafny
• RAHFT
• ProB
• Spacer
• Zeno
• HipSpec
• VeriMAP
• CVC4
• z3
• IsaPlanner
• PVS
• OCaml
• MathSAT5

This page was built for publication: Removing algebraic data types from constrained Horn clauses using difference predicates

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096439)