Presentation

The goal of this project is the verification of C programs that are used to control safety-critical systems, such as airplanes, subway lines or power plants.

Within the past decade, push-button verification techniques (e.g. model checking, SAT solving, etc.) have become commonplace in the development of hardware systems. An integration of such methods within the development of software systems is highly required by the manufacturers of critical and embedded systems (avionics, telecommunications, public transport, etc.). Indeed, software programs used for the control of safety-critical systems (e.g., airplanes, trains, power plants, etc.) are required nowadays, by the certification authorities, to undergo formal verification, in order to ensure absence of run-time errors (e.g., null pointer exceptions, memory leaks, arithmetic exceptions, etc.). Such errors have caused in the past considerable losses, both economical and human (e.g., the crash of ESA/ARIANE 5 maiden flight, due to an arithmetic exception).

The goal of this project is the verification of C programs that are used to control safety-critical systems, such as power plants. A major problem is the scalability of existing verification techniques for programs with dynamic data structures. These techniques are capable nowadays of analyzing and finding bugs in toy programs of about 100 lines of code. In this project we aim, on one hand, at extending the existing verification techniques in order to deal with parallel programs handling singly-linked lists and array data structures. On the other hand, we aim at applying these techniques to real-life test cases with several thousands lines of C code. The project follows two main directions:

• • Model extraction from C programs This direction will use slicing and abstraction techniques for parallel programs, in order to eliminate parts of code which are irrelevant for the properties verified. These properties include memory violations (e.g. null pointer exceptions, memory leaks, etc.). deadlocks (in case of concurrent programs) and out of bounds array accesses.

  • Verification of memory consistency properties Existing verification techniques are capable of dealing with sequential programs handling lists and arrays of integers. One of our goals is extending the existing techniques to multi-threading programs using lock-based synchronization mechanisms, as it is usually the case in C applications.

The final result of the project will be a prototype tool capable of analyzing an important number of test cases, provided by the industrial partners (in particular, EDF)