Verifying Catamorphism-Based Contracts using Constrained Horn Clauses

DOI10.1017/S1471068422000175MaRDI QIDQ5038461zbMATH OpenFDO

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

Publication date 30 September 2022

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

analysis and verification of systemsconstraintssecurityspecificationtheory

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach
• Solving constrained Horn clauses over algebraic data types
• Solving Horn clauses on inductive data types without induction
• Relational verification through Horn clause transformation

Cites work

• A transformational approach to resource analysis with typed-norms inference
• An axiomatic basis for computer programming
• An overview of Ciao and its design philosophy
• Automating induction for solving Horn clauses
• Decision procedures for algebraic data types with abstractions
• Fold/unfold transformations for fixpoint logic
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 3848583 (Why is no real title available?)
• Induction for SMT solvers
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• Reasoning about algebraic data types with abstractions
• Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach
• SMT-based model checking for recursive programs
• Solving Horn clauses on inductive data types without induction
• Synchronizing constrained Horn clauses
• Transformations of CLP modules
• Unifying structured recursion schemes
• Why3 -- where programs meet provers

Cited in

(5)

• Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach
• scientific article; zbMATH DE number 7806141 (Why is no real title available?)
• Automatic program instrumentation for automatic verification
• Catamorphic abstractions for constrained Horn clause satisfiability
• A program instrumentation framework for automatic verification

Describes a project that uses

Uses Software

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

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

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