Predicate pairing for program verification

DOI10.1017/S1471068417000497zbMATH Open1478.68153arXiv1708.01473MaRDI QIDQ4644353FDOQ4644353

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

Publication date: 31 May 2018

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

Abstract: It is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for CHCs (CHC solvers) based on predicate abstraction are sometimes unable to verify satisfiability because they look for models that are definable in a given class A of constraints, called A-definable models. We introduce a transformation technique, called Predicate Pairing (PP), which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an A-definable model, and hence can be effectively verified by CHC solvers. We prove that, under very general conditions on A, the unfold/fold transformation rules preserve the existence of an A-definable model, i.e., if the original clauses have an A-definable model, then the transformed clauses have an A-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an A-definable model iff the original ones have an A-definable model. Then, we present the PP strategy which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability can be proved by looking for A-definable models. PP introduces a new predicate defined by the conjunction of two predicates together with some constraints. We show through some examples that an A-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We also present some case studies showing that PP plays a crucial role in the verification of relational properties of programs (e.g., program equivalence and non-interference). Finally, we perform an experimental evaluation to assess the effectiveness of PP in increasing the power of CHC solving.

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

Recommendations

• Predicate pairing with abstraction for relational verification
• Relational verification through Horn clause transformation
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Probabilistic Horn clause verification
• Constraint-based relational verification

zbMATH Keywords

constraint logic programmingprogram verificationprogram transformationconstrained Horn clausesrelational properties of programs

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• The octagon abstract domain
• Regression verification for unbalanced recursive functions
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Title not available (Why is that?)
• Transformation of logic programs: Foundations and techniques
• Verification, Model Checking, and Abstract Interpretation
• Regression verification for multi-threaded programs
• Inference rules for proving the equivalence of recursive procedures
• Simple relational correctness proofs for static analyses and program transformations
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Conjunctive partial deduction: foundations, control, algorithms, and experiments
• Logic program specialisation through partial deduction: Control issues
• Title not available (Why is that?)
• Transformations of CLP modules
• Abstract interpretation of logic programs using magic transformations
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• A rule-based verification strategy for array manipulating programs
• Horn clause solvers for program verification
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Relational verification through Horn clause transformation
• Property directed equivalence via abstract simulation
• Underapproximation of procedure summaries for integer programs

Cited In (8)

• Title not available (Why is that?)
• Constraint-based relational verification
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Predicate signatures from pair encodings via dual system proof technique
• Title not available (Why is that?)
• Relational verification through Horn clause transformation
• Predicate pairing with abstraction for relational verification
• Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification

Uses Software

• ECCE

This page was built for publication: Predicate pairing for program verification

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