Cross theory rigorous program verification using Constrained Horn clauses

State-of-the-art approaches to automated software verification delegate the computational tasks to solvers for Satisfiability Modulo Theories (SMT) and Constrained Horn Clauses (CHC). The latter enables synthesizing inductive invariants and offers sound but possibly incomplete reasoning about software. Existing approaches to solve CHC either heavily approximate the systems or reduce the analysis to their snippets, thus being unable to verify real-world systems.

The goal of our project is to develop a novel CHC-based verification framework for handling complex programs symbolically and efficiently. We aim at preserving sufficient level of details meaningful for the program developers and users. The project will deliver a set of automated techniques that rely on existing CHC solvers developed by the PI from USI and the partner from Florida State University in the USA. The complementary strengths of these solvers will be combined in a new cross-theory framework that lazily enumerates the theories used in the CHC encoding and applies appropriate techniques provided by the solvers for those theories.

Specifically, the work proposes using the Golem and FreqHorn CHC solvers as starting points for developing a new CHC-solving technology. Golem has the implementations of various efficient algorithms and utilizes Craig interpolation to discover invariants in linear arithmetic. FreqHorn uses the enumerative search boosted by deductive reasoning, and it discovers quantified invariants over arrays. Although our solutions will be well suited for implementation on top of Golem and FreqHorn, they will be generic and potentially realizable on top of other solvers.

We will deliver open-source tools and evaluate them on CHC systems that originate from software from academia and industry. The emphasis will be made on verification of Ethereum smart contracts provided by the industrial partner. The proposal will advance tools for software verification and enable automated reasoning w.r.t. safety properties that otherwise would require many human efforts.