In recent years, there has been a rise of programming languages that mix traditional imperative approaches to programming with features from functional languages, in particular, with algebraic data types (ADTs) and pattern matching. Notable examples of languages in this class include Scala, Kotlin, Swift and Rust. Structured state is here represented using immutable values instead of references on a mutable heap. This avoids many of the pitfalls (in particular, aliasing and the frame problem) that accompany the formal verification of heap-manipulating programs.

At the same time, automatic verification of functional and relational program properties using predicate inference for constrained Horn clauses have become increasingly popular and successful. Automatic verification of heap-manipulating programs is a difficult task such that the rise of ADTs in imperative programming languages provides an opportunity to automatically verify programs with expressive data types besides heap manipulation. We present an approach with which imperative programs that employ values of user-defined algebraic data types can be automatically verified. To achieve this goal, the approach encodes verification conditions as sets of constraint Horn clauses and then infers inductive predicates that solve the clauses by a technique extending the successful ICE framework for predicate inference.

The approach can be used to automatically prove equivalence of programs using ADTs. The implementation has been applied to a few non-trivial program equivalence examples, one of which is shown here.