Candidate: Hari Govind V K
Title: Towards Scalable Fully Automatic Program Verification
Date: June 10, 2024
Time: 2:00 PM
Place: EIT 3142
Supervisor(s): Gurfinkel, Arie
Abstract:
Formal verification is a rigorous way to establish software quality. After more than 50 years of research, we are at a point where formal verification is starting to be used in industrial applications. To encourage more adoption, we need to automate formal verification techniques as much as possible so that even users who are not familiar with formal verification can use it to ensure software quality. Many automatic verification tasks are reducible to the problem of satisfiability checking of Constrained Horn Clauses (CHCs) modulo background theories. The list includes safety verification of imperative and functional programs, regression verification, static analysis, refinement type inference, and many more. Motivated by the number of applications, we explore advancements to CHC solving.
We make three contributions to improving the state of the art in CHC solving. First, we study the problem of lemma generalization inside CHC solvers. State of the art CHC solvers construct solutions to CHCs by learning several lemmas, each of which block parts of the search space, and together form a complete solution. However, the generalization strategies that CHC solvers employ during lemma learning are local: they are unaware of the solution that CHC solver is constructing. This causes CHC solvers to diverge and worse, be susceptible to syntactic changes in the input. We mitigate the effects of local generalization by identifying patterns in lemmas learned during CHC solving and enforcing course correction during CHC solving via a process called global guidance. We instantiate global guidance inside the Spacer CHC solver and show that it improves Spacer on a variety of benchmarks and makes Spacer agnostic to local generalization strategies.
In the second part of the thesis, we look at CHC solving in the context of safety verification of programs manipulating user-defined recursive datatypes like lists and trees. The invariants of such programs typically require recursive functions as well. This domain is particularly hard for CHC solvers because the presence of recursive functions makes even validating solutions to CHCs undecidable. We propose a new approach that sidesteps the undecidability by abstracting recursive functions using uninterpreted functions when validating solutions. We show the typical approach to overcome this undecidability, that of eliminating recursive functions by encoding them as a set of CHCs, loses solutions and is therefore infeasible for many CHC solvers.
In the third part of the thesis, we go deeper inside CHC solvers and propose algorithmic improvements to the solutions to two important subproblems encountered during CHC solving: modular solving and approximations of quantifier elimination.