Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
From MaRDI portal
Publication:5038461
DOI10.1017/S1471068422000175MaRDI QIDQ5038461FDOQ5038461
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)
Full work available at URL: https://arxiv.org/abs/2205.06236
Recommendations
Cites Work
- Why3 -- where programs meet provers
- Induction for SMT solvers
- An axiomatic basis for computer programming
- An overview of Ciao and its design philosophy
- SMT-based model checking for recursive programs
- Transformations of CLP modules
- Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
- Automating induction for solving Horn clauses
- Horn clause solvers for program verification
- Fold/unfold transformations for fixpoint logic
- Title not available (Why is that?)
- Reasoning about algebraic data types with abstractions
- Decision procedures for algebraic data types with abstractions
- Solving Horn clauses on inductive data types without induction
- Synchronizing constrained Horn clauses
- A transformational approach to resource analysis with typed-norms inference
- Unifying structured recursion schemes
- Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach
Cited In (2)
Uses Software
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)
