Predicate pairing for program verification

DOI10.1017/S1471068417000497MaRDI QIDQ4644353zbMATH OpenFDO

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)

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

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)

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.

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

Cites work

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

Cited in

(8)

• scientific article; zbMATH DE number 7447758 (Why is no real title available?)
• Constraint-based relational verification
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Predicate signatures from pair encodings via dual system proof technique
• scientific article; zbMATH DE number 7444023 (Why is no real title available?)
• 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

Describes a project that uses

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)