Participants

The Institut National de Recherche en Informatique et Automation (INRIA) participates with members based at its Saclay site, belonging to the following INRIA reasearch projects-teams:

COMETE: the INRIA project called COMETE focuses on the design, implementation and applications of formal languages for mobile, secure, stochastic and distributed systems of the kind considered by Panda. Its members are particularly interested in formal languages based on process calculi.
The following software will be used in PANDA:

• a model checker for the probabilistic asynchronous π-calculus;
• the PRISM model generator;
• tools calculating the set of corner points of a channel.

PARSIFAL: the PARSIFAL project-team aims at elaborating methods and tools for specifying and reasoning about computation systems, such as, for example, compilers, security protocols, and concurrent programs. A central challenge here is proving properties of programs that manipulate other programs.
PARSIFAL has implemented three software systems:

• Abella,
• Tac,
• Bedwyr.

• Catuscia Palamidessi (project leader)
• Christelle Braun
• Dale Miller
• Frank Valencia

The Commissariat à l'Energie Atomique (CEA) participates with members from its LIST laboratory, in particular with its team MeASI (Modélisation et Analyse des Systèmes en Interaction).

The MeASI team focuses on theoretical research on methods for static analysis, along with the development of applications of related software tools. The ALCOOL group (which is also the name of the software developed by the group) is specialized in the analysis of concurrency and parallelism through techniques coming from directed algebraic topology. Together with this, the ALCOOL group has also expertise in software development (mostly using OCaml).

Within the Panda project, the ALCOOL group will compare its approach to concurrency to other more traditional approaches, which do not make explicit use of topological notions.

The Panda project is also an opportunity to confront the ALCOOL toolbox with new case studies originating from the industrial world (in particular those provided by Airbus), in order to enhance its development.

The development of the ALCOOL software has been supported for several years by EDF, and is at present going towards the introduction of libraries (to be developed within the Panda project) based on the most recent advances in the domain of directed albegraic topology and concurrency.

• Emmanuel Haucourt (site coordinator)
• Eric Goubault
• Samuel Mimram
• Tobias Heindel (post-doc grant provided by ANR through the Panda project)

The pôle parisien is a group of researchers belonging to laboratories situated for the most part in the Paris area. It is coordinated by Université Paris Nord - Paris 13.

LIPN: The Laboratoire d'Informatique de Paris Nord (LIPN) is the coordinator of the pôle parisien. LIPN plays a major role in research in computer science within the northern Paris area; in particular, the Panda project touches several topics which are developed at LIPN within its Logic, Computation, and Reasoning team. These include linear logic proof theory, interaction nets and, more generally, rewriting theory, and all their applications to concurrency.

PPS: The laboratory Preuves, Programmes et Systèmes federates the energies of researchers coming from different cultures (computer science and mathematical logic) to work on the logical foundations of programming languages and distributed systems. Within Panda, PPS contributes with research spanning from logic (and, in particular, proof theory) to category theory, from homology and homotopy to probability theory, with the aim of providing a clearer understanding of distributed programs and guaranteeing their correctness.

LSV: The Laboratoire Spécification et Vérification (LSV) is the computer science laboratory of ENS Cachan. LSV devotes most of its research efforts to the study of the specification and verification of critical systems, with the aim of developing languages and formal methods for expressing and proving correctness of those systems. LSV participates to Panda with members of its research group INFINI, which focuses on verifying infinite systems: programs that manipulate unbounded values, recursive communicating processes, parametrized systems. Members of the INFINI group also develop software tools for program verification; we mention in particular the following, whose development is relevant to the Panda project:

• TOPICS, a tool for analysing programs manipulating lists and counters;
• heaphop, a tool for analyzing concurrent programs which manipulate lists and trees, and synchronize through Hoare monitors or message passing.

LIP and LAMA: Even though they are not situated in the Paris area, the Laboratoire de l'Informatique du Parallélisme (LIP, ENS Lyon) and the Department of Mathematics of the Université de Savoie (LAMA) contribute to the Panda project with research in the main theoretical fields developed by the pôle parisien. In particular, researchers at LIP and LAMA have a specific expertise in proof theory, games semantics, and formal semantics of concurrent programming languages.

• Damiano Mazza (LIPN, site coordinator)
• Samy Abbes (PPS)
• Andrei Dorman (LIPN)
• Daniel Hirschkoff (LIP)
• Tom Hirschowitz (LAMA)
• Etienne Lozes (LSV)
• Paul-Andrê Melliès (PPS)
• Christine Tasson (PPS)
• Jules Villard (formerly at LSV, now Queen Mary)

The pôle méditerranéen comprises researchers belonging to laboratories situated in Marseille. It is coordinated by Université de Provence - Aix-Marseille 1.

The two laboratories involved are the Laboratoire d'Informatique Fondamentale (LIF, Université Aix-Marseille 1, the coordinator of the pôle méditerranéen) and the Institut de Mathématiques de Luminy (IML, Université Aix-Marseille 2). The contribution of the Panda members belonging to the pôle méditerranéen is mostly theoretical, and is focused on the following research axes:

• verification;
• distributed algorithms;
• denotational semantics of concurrent languages.

• Emmanuel Godard (LIF, site coordinator)
• Emmanuel Beffara (IML)

Airbus is one of the world leading companies in the production of commercial aircrafts and avionic systems. Its contribution to the Panda project is to provide the other reaserch partners with distributed software of industrial origin on which the tools developed by the project may be modeled and tested.

• Jean Souyris (site coordinator)