Specification Synthesis with Constrained Horn Clauses

Includes bibliographical reference

PhD;2023;Computer Science and Automation

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-CheckWeaken 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
ii
Abstract
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 FloydHoare 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.