Verifying Catamorphism-Based Contracts using Constrained Horn Clauses

DOI10.1017/S1471068422000175MaRDI QIDQ5038461

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

Publication date: 30 September 2022

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

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

zbMATH Keywords

securityconstraintsspecificationtheoryanalysis and verification of systems

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items (1)

Unnamed Item

Uses Software

• Why3
• z3
• Scala
• Boogie
• CVC4
• WhyML
• Ciao
• CiaoPP
• Spacer
• VeriMAP

Cites Work

• Unnamed Item
• SMT-based model checking for recursive programs
• Transformations of CLP modules
• Reasoning about algebraic data types with abstractions
• Automating induction for solving Horn clauses
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• An overview of Ciao and its design philosophy
• Horn Clause Solvers for Program Verification
• Solving Horn Clauses on Inductive Data Types Without Induction
• Synchronizing Constrained Horn Clauses
• A Transformational Approach to Resource Analysis with Typed-norms Inference
• Fold/Unfold Transformations for Fixpoint Logic
• Induction for SMT Solvers
• Unifying structured recursion schemes
• Decision procedures for algebraic data types with abstractions
• Why3 — Where Programs Meet Provers
• An axiomatic basis for computer programming
• Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach

This page was built for publication: Verifying Catamorphism-Based Contracts using Constrained Horn Clauses