PANDA

A great deal of control-command systems are parallel programs (sometimes based on the synchronous paradigm, but not always), or distributed applications (due in particular to specifics of fault-tolerance programming). In general, formal methods, or static analysis has been used in this context to validate these systems by making simplifying assumptions on the scheduling of the different parallel tasks. If these hypotheses are generally satisfied in very critical systems (very strong synchronisations are required, which make the concurrent program ``equivalent'' to a sequential one), it is not the case for less critical systems, more asynchronous and non-deterministic in general. Whatever concrete model of computation we use, the validation of concurrent and distributed programs is difficult because the number of its accessible states is too important to be enumerated, and even the number of control points, on which any abstract collecting semantics is based, explodes. This is due to the great number of distinct scheduling of actions in legal executions. This adds up to the important size of the codes, which, because they are less critical, are more often bigger. The objective of this project is to develop theories and tools allowing for tackling this combinatorial explosion, in order to validate concurrent and distributed programs by static analysis, in an efficient manner. Our primary interest lies in multithreaded shared memory systems. But we want to consider a number of other paradigms of computations, encompassing most of the classical ones (message-passing for instance as in POSIX or VXWORKS) as well as more recent ones such as the ones found in Singularity for instance, which will provide a good ``test case'' for the formal semantics and methods the project is aiming at developping. Last but not least, we want to show that our approaches for comparisons of models and derived static analyses does work well in practise. We rely on industrial codes for experimentation, such as the ones provided by Airbus, but also on other academic codes, that partners generally use for their own benchmarks. We plan on disseminating part of the results of this project both as usual through conferences of the best international standard but also by providing some of our implementations in open source to a larger community.