Property Directed Inference of Relational Invariants

Property Directed Reachability (PDR) is an efficient and scalable approach for solving systems of symbolic constraints, also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for each uninterpreted predicate. However, in many practical cases, this reasoning is not successful, as invariants need to be discovered for groups of predicates, as opposed to individual predicates. We contribute a novel algorithm that identifies such groups automatically and complements the existing PDR technique. The key feature of the algorithm is that it does not require a possibly expensive synchronization transformation over the system of CHCs. We have implemented the algorithm on top of a state-of the-art CHC solver SPACER. Our experimental evaluation shows that for some CHC systems, on which existing solvers diverge, our tool is able to discover relational invariants.