The Panda project is composed of 4 academic research partners (INRIA Saclay, CEA LIST, pôle parisien, pôle méditerranéen) and 1 industrial partner (Airbus).


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.
They are all open source systems. Short descriptions for them are available here.
People involved: Additionally, INRIA Saclay hired a Ph.D. student on a grant provided by ANR through the Panda project.


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.

People involved:

Paris 13
Pôle parisien

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.

People involved:

  Aix-Marseille 1
Pôle méditerranéen

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.
In particular, the study aims at providing formal models for computational systems (programs, distributed systems, etc.) and devise algorithms allowing the verification of properties of such systems. The mathematical tools involved come from graph combinatorics, topology, geometry, and also from proof theory, category theory, domain theory, and general denotational semantics.
People involved:

Airbus Airbus

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.

People involved:
  • Jean Souyris (site coordinator)