Tags:algebraic data types, CEGAR, collaborative inference, constrained Horn clauses and inductive invariants
Abstract:
Inductive invariant inference is the core problem of program verification, in particular, verification of functional programs over algebraic data types (ADTs). This problem is even more complex for the case of ADTs as it is hard to come up with an abstract domain rich enough to represent properties of practical programs and an effective invariant inference procedure for this domain. Many complementary techniques for different abstract domains for ADTs were developed, yet corresponding tools often diverge on real-life programs because of low expressivity of their abstract domains. Moreover, it was unclear whether they could complement each other. We propose a lightweight approach for combining any existing techniques for different abstract domains collaboratively, i.e., a non-portfolio approach for building a verifier with a more expressive domain from existing verifiers. We instantiate it and obtain an effective inductive invariant inference algorithm in a rich combined domain of elementary and regular ADT invariants essentially for free. Because of the richer domain, collaborations of verifiers converge on strictly larger numbers of safety problems, i.e., the collaboration of verifiers is capable of solving problems that are beyond their abilities on their own. Our implementation of the algorithm is a collaboration of two existing state-of-art inductive invariant inference engines having general-purpose first-order logic solvers as a backend. Finally, we show that our implementation is capable of solving the large amount of CHC-Comp 2022 problems obtained from Haskell verification problems, for which the existing tools diverge.