Predicate Pairing for program verification
From MaRDI portal
Publication:4644353
DOI10.1017/S1471068417000497zbMath1478.68153arXiv1708.01473MaRDI QIDQ4644353
Alberto Pettorossi, Emanuele De Angelis, Maurizio Proietti, Fabio Fioravanti
Publication date: 31 May 2018
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1708.01473
program transformationconstraint logic programmingprogram verificationconstrained Horn clausesrelational properties of programs
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)
Related Items (3)
Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Transformations of CLP modules
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- The octagon abstract domain
- Inference rules for proving the equivalence of recursive procedures
- Relational verification through Horn clause transformation
- Regression verification for unbalanced recursive functions
- Regression Verification for Multi-threaded Programs
- Horn Clause Solvers for Program Verification
- A Rule-based Verification Strategy for Array Manipulating Programs
- Simple relational correctness proofs for static analyses and program transformations
- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
- Abstract interpretation of logic programs using magic transformations
- Transformation of logic programs: Foundations and techniques
- Logic program specialisation through partial deduction: Control issues
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Property Directed Equivalence via Abstract Simulation
- Conjunctive partial deduction: foundations, control, algorithms, and experiments
- Underapproximation of Procedure Summaries for Integer Programs
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- An axiomatic basis for computer programming
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Predicate Pairing for program verification
