Automatic verification of higher-order functional programs using regular tree languages
Timothée Haudebourg · HAL (Le Centre pour la Communication Scientifique Directe) · 2020
This thesis studies how regular tree languages can be used to automatically verify properties on higher-order functional programs. Our goal is to develop new techniques and tools for the programmers to develop safer programs while reducing the time and expertise needed to verify them. In particular, we focus on the automatic verification of regular safety properties, a family of properties for which we show that completely and fully automatic verification can be achieved. Our verification method is build upon a regular abstraction procedure that can automatically learn regular tree languages that over-approximates of the reachable states of a program, allowing the verification of a target property. By using regular languages as types we modularize this procedure to verify complex properties by stating them as type inference problems. In addition we study the performances of the overall technique in our prototype OCaml implementation in the Timbuk4 verification framework over a test suite of more than 80 verification problems. We then show how our abstraction procedure can be used to verify relational properties that seemed out of the scope of regular tree languages. To do that, we use and extend a convolution operator on trees to represent every element of a relation into a regular tree language. We can then extend our previously defied regular language learning procedure to automatically infer such regular relations. We propose a Rust implementation of this idea as a regular solver for Constrained Horn Clauses systems and study its performance on several relational verification problems.