Specification Synthesis with Constrained Horn Clauses

Abstract

Many practical problems in software development, verification and testing rely on specifications. The problem of specification synthesis is to automatically find relational constraints for undefined functions, called specifications, in a given program and a postcondition. Specifications are helpful in verifying open programs, compositional verification, automatic test case generation, run-time checks, program understanding and many more applications. Maximal (or logically weakest) specifications are desirable in all these applications. The specifications also have to be valid with respect to the given program's semantics and the postcondition.

Existing tools expect the developers of programs to provide specifications. Providing specifications is tedious for developers, hindering the wide adoption of program verification and synthesis tools. Automatic synthesis of valid and maximal specifications is beneficial; but has several challenges. This thesis proposes techniques to overcome the challenges.

The techniques work in a framework called Infer-Check-Weaken, using which valid and maximal specifications are effectively synthesised. The core idea behind Infer-Check-Weaken is first to infer a valid specification. Then, in a loop, the specification is checked for maximality. When the check fails, weakening is performed. This loop continues till a maximal specification is obtained. Depending on the specifications to be inferred and the structure of the programs, we propose different techniques to perform each task. We show the effectiveness of these techniques over publicly available benchmarks.

More specifically, for programs with integer variables and linear arithmetic operations, we propose an inference technique called Non-vacuous Specification Synthesis (NSS), which can find specifications like function contracts on undefined functions, preconditions, and others along with inductive invariants. NSS works on the idea of backward and forward reasoning. The maximality checking is performed by encoding the problem as a logical formula and then using an SMT solver. Further, weakening is done using the feedback from maximality checking and the NSS module.

This thesis's second and third contributions are in finding the weakest precondition for deterministic and non-deterministic terminating programs that manipulate arrays. Such programs often require quantified preconditions, which are difficult to reason about. To infer quantified preconditions, we propose two techniques: Range Abduction (RA) and its extension Structural Array Abduction (SAA). RA extends the logical abduction to quantified formulas over arrays. SAA further extends RA to find proof of maximality additionally. We propose different maximality-checking techniques for deterministic and non-deterministic programs based on program transformation and a syntax-guided-synthesis-based weakening procedure.

These techniques work at the level of a logical intermediate representation in the Floyd-Hoare style, making them agnostic to programming languages. The intermediate representation is called constrained Horn clauses, which are gaining popularity among various program verification tools. Hence, our techniques can be integrated with the existing tools.