Synchronizing Constraint Horn Clauses

Abstract:

The goal of unbounded program verification is to discover an inductive invariant that over-approximates all reachable program states and is precise enough to exclude all bad states. State-of-the-art approaches to invariant synthesis proceed by 1) encoding the program to a system of Constrained Horn clauses (CHC) and 2) employing an SMT-based procedure to check satisfiability of CHCs. However, a solution of such a system is often inexpressible in the constraint language, especially if the program suffers of multiple recursive calls operating on the shared data. We propose to synchronize recurrent computations, thus increasing the chances for an invariant to be found.

Our novel notion of the CHC product gives rise to a lightweight iterative algorithm of merging recurrent computations into groups and its applications to automated program synthesis. In particular, we applied the CHC-product transformation to certify solutions delivered by our automatic parallelization tool, called GraSSP. Given an arbitrary segmentation of the input data, GraSSP synthesizes a code to determine a new segmentation of that data which allows computing partial results for each segment and finally merging them. The talk will focus on the practical aspects of GraSSP, and on verification of a wider range of recursive programs that became possible after applying the CHC-product transformation.

Biography:

Grigory Fedyukovich is a postdoc at Princeton University, USA, working with Prof. Aarti Gupta. He graduated from UniversitÀ della Svizzera italiana, Switzerland, under supervision of Prof. Natasha Sharygina and completed a postdoc at University of Washington with Prof. Rastislav Bodik. His main research interests are in the areas of Symbolic Model Checking, Automated Program Synthesis, and Program Equivalence.