Predicate Pairing for program verification

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

zbMATH Keywords

program transformationconstraint logic programmingprogram verificationconstrained Horn clausesrelational properties of programs

Mathematics Subject Classification ID

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

• ECCE

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