Analysis and Verification of Critical Concurrent Programs

Project Summary

The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which is regulated by norms that advise or enforce the use of formal or semi-formal validation techniques. Academic researchers are being led to collaborate with industry in the development of methods and tools that allow practitioners to incorporate formal verification in their validation process.

This project stems from an ongoing collaboration between three academic groups and software engineers working for companies that work precisely in safety-sensitive domains, subject to norms such as mentioned above.

After enormous developments in the verification of sequential software, industry is now able to employ formal verification techniques in their projects, either based on model checking, abstract interpretation, or logical proofs. Unfortunately, safety-critical applications are usually inherently concurrent, which means that these are often of limited utility. Moreover, there is a mismatach between the programming languages that are receiving more attention from the research community and those that are used in practice in the safety-critical domain. Ada for instance, has paradoxically fallen out of fashion as a general purpose programming language, but is more and more used in the safety-critical domain (a fact of which academics are seldom aware). The languages that will be object of our study will include at least a subset of C and the RavenSPARK high integrity language, both widely used by practitioners in the critical domain.

The scope of the present project is the verification of properties of shared memory concurrent programs, both advancing the state of the art at the theoretical level and producing tools that can be used by companies developing critical applications. Our approach will focus simultaneously on two techniques: software model checking and deductive reasoning. Crucially, advances in each technique have historically fed back into the other technique, and we believe such a mixed approach (which is made possible by the know-how accumulated by the team over the last five years) can be fruitful.


The goals of the project are (labelled [T]heoretical or [P]ractical):

1. [T] To investigate abstraction techniques that can be used to tame the state explosion problem inherent to any programming language with a realistic set of types. For this we will build on recent work, in particular on predicate abstraction. We hope to be able to propose enhancements to the published abstraction mechanisms, in particular stemming from the work on deductive compositional verification methods that will take place in parallel (see below).

It is not our goal to investigate model checking algorithms; our interest is in the extraction of approximated models from the source code and in checking properties of these models using a standard model checker. This allows us to automatically take benefit from the wealth of work accumulated on taming other sources of state explosion like control flow.

2. [P] (building on 1) To produce software model checking tools for our object languages. The approach to be followed can be summarized as follows: we will perform syntactical analysis of the source code, and apply abstraction techniques to obtain the control flow graph of an approximated version of the initial program. From this we will produce a Labelled Transitions (LT) model. The tool will also translate properties (expressed as comments in the source code) to properties expressed in the logic of the model checker, that can be used to query it.

3. [P] (building on 2) To investigate the possibility of producing a common language for representing LT systems and properties of these systems. The idea would be that these models and properties can then be exported to more than one model checking tool. It may well be the case that some properties can be checked with one model checker, while another checker may be able to check other properties. In this generic approach we take inspiration from tools for deductive verification of sequential programs, like Why and Boogie.

4. [T,P] To propose a verification conditions generator (VCGen) for a (concurrent) subset of one of our object languages, based on rely-guarantee principles. The subset will be sufficiently simple to allow us to focus on the generation of verification conditions, and to put together a complete verification platform, consisting of the VCGen and a choice of SMT solvers to discharge the VCs.

5. [T] (building on 4) To study extensions of the rely-guarantee system to accommodate progressively richer features of the programming language, including heap-based dynamic structures. We will consider in particular combinations with formalisms like separation logic and typed memory.

r1 - 18 Feb 2013 - 18:51:40 - JorgeSousaPinto
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM