Software Verification and Synthesis using Constraints and Program Transformation

Emanuele De Angelis
University “G. D’Annunzio” of Chieti-Pescara
April 2014

ABSTRACT

In the last decade formal methods applied to software production have received a renewed attention as the basis of a methodology for increasing the reliability of software artefacts (for example, source code) and reducing the cost of software production (for example, by reducing the time to market). In particular, a massive effort has been made to devise automatic techniques, such as software model checking, for reasoning about the correctness of programs with respect to their specifications. A complementary approach to program verification is represented by program synthesis, which, starting from a formal specification of the intended behaviour, has the objective of automatically deriving a program that complies with the given specification. However, program synthesis does not represent an alternative to verification in all cases and is much harder to put in practice, especially when scalability becomes a critical factor.

The thesis deals with program verification and synthesis by applying automated reasoning techniques based on logic programming.

The first contribution of the thesis concerns the design of a general verification framework and its implementation to perform software model checking of imperative programs. In particular, we have considered program transformation and Constraint Logic Programming (CLP) as foundational building blocks to define a verification framework which is parametric with respect to the various syntaxes and semantics of the programming languages under consideration and also to the various logics in which the properties of interest may be expressed. Let us summarize here the main contributions with regard to program verification.

  1. The adaptation and the integration of various techniques for specializing and transforming constraint logic programs into a general verification framework, where the generation of the verification conditions, that express the correctness of a given program, and their verification can both be viewed as program transformation of constraint logic programs. This adaptation has required the customization of general purpose unfolding and generalization strategies to the specific task of specializing the interpreter of the programming language under consideration, as well as the programs derived from the interpreter in subsequent iterations of the verification method. In particular, we have adapted to our context suitable strategies, based on operators often used in static program analysis such as widening and convex-hull, for the automatic
    discovery of loop invariants of the imperative programs to be verified.
  2. The implementation of the verification framework into a prototype automatic tool, called VeriMAP, based on the C Intermediate Language (CIL) front-end (http://kerneis.github.io/cil/) and the MAP transformation system for constraint logic programs (http://www.iasi.cnr.it/~proietti/system.html). The VeriMAP tool is available at http://map.uniroma2.it/VeriMAP.
  3. We have considered a significant fragment of the C Language, and we have shown, through an extensive experimental evaluation on a large set of examples taken from different sources (programs manipulating integers and integer arrays), that our approach,
    despite its generality, is also effective and efficient in practice.

The thesis also deals with the problem of program synthesis by using, as done for program verification, techniques based on logic and constraint solving. Indeed, the second contribution
of the thesis is a synthesis framework, based on Answer Set Programming (ASP), for the automatic derivation of synchronization protocols for concurrent programs satisfying some given behavioural and structural properties. In particular, design of protocols is reduced to finding models, also called answer sets, of the logic program that encodes the behavioural properties, such as mutual exclusion, specified by formulas of the Computational Tree Logic and structural properties are specified by simple algebraic structures. The desired behavioural and structural properties are encoded as logic programs which are given as input to an ASP solver which, then, computes the answer sets of those programs. Every answer set encodes a concurrent program satisfying the given properties. Then, the different protocols satisfying the given specification can be derived by a simple decoding of the computed answer sets. The advantage of the presented method resides in the fact that we deal with the synthesis problem in a purely declarative manner, by reducing the problem of synthesizing a synchronization protocol to the problem of finding the answer sets of a logic program encoding a given specification. The framework makes use of the on-the-shelf ASP solvers, such as claspD and DLV. Moreover, we have proved that our synthesis procedure has optimal time complexity because it has EXPTIME com- plexity with respect to the size of the temporal specification, and thus, it matches the complexity of the synthesis problem.

FULL TEXT