Parallelism and Security
Key personnel: G. Barthe, G. Boudol
Work on concurrency theory in the PPS Laboratory focuses on basic models of interactive computation such as the pi-calculus. One general goal is to connect this and related operational models of concurrency to models which are simpler and/or offer a richer mathematical framework such as event structures, game models, and interaction nets. In another direction, which is not directly relevant for the ParSec project, we develop formal models of biological system. A specific goal we address in the context of the ParSec projet is to study the semantic foundations of a pi-calculus in a synchronous execution scenario and to analyse determinacy, resource control, and information flow issues in this setting.
Key personnel: R. Amadio, D. Varacca
The MOSCOVA research team has a renowed competence in the design and implementation of programming languages for distributed systems (JoCaml, Acute), and in the validation and the debugging of real concurrent programs, such as the CAML concurrent garbage collector or the Ariane-5 rocket on board software. The Moscova research team will contribute to ParSec by studying and implementing logics for reliable concurrent programs and secure information flow.
Key personnel: J-J. Lévy, F. Zappa Nardelli
The Lande project is concerned with formal methods for constructing and validating software. Our focus is on providing methods with a solid formal basis (in the form of a precise semantics for the programming language used and a formal logic for specifying properties of programs) in order to provide firm guarantees as to their correctness. In addition, it is important that the provided methods are highly automated so as to be usable by non-experts in formal methods. The Lande research team will contribute to ParSec by studying the availability aspect of security in the context of concurrent programs.
Key personnel: F. Besson, T. Jensen, D. Pichardie