David Chemouil

Picture of David Chemouil

David Chemouil
Computer Scientist (PhD, habil.)

2 avenue Édouard Belin, 31055 Toulouse, France

Tel: +33 (0) 5 6225 2936
Mail: firstName.lastName@onera.fr


  • 01/2017: two PhD propositions: one on the efficient verification of first-order temporal specifications, and another one on the formal specification and verification of a language dedicated to the design of user interfaces for critical applications.
  • 01/2017: habilitation passed.
  • 06/2016: paper On Finite Domains in First-Order Linear Temporal Logic accepted at ATVA 2016.
  • 06/2016: paper Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations accepted at FSE 2016.


Publications? see below (you may also see DBLP and HAL, many thanks to them)

Current topics

  • My main research purpose is to build bridges between theoretical computer science and software engineering, e.g.:
    • Multi-agent temporal logic for goal- and agent-oriented requirements modeling.
    • Relational first-order temporal logic for lightweight specification and verification and for safety & security assessment of critical systems.
  • I also maintain a longing, but hitherto little explored, interest for applications of functional programming, categorical methods and type systems in the context of software engineering.
  • Some collaborators: Julien Brunel (ONERA), Christophe Chareton (LORIA), Denis Kuperberg (ENS Lyon), Alcino Cunha (U. Braga), Nuno Macedo (U. Braga), Mamoun Filali (IRIT), Jean-Paul Bodeveix (IRIT)

PhD students and Postdoctoral researchers


  • Jeanne Tawa (PhD student, co-promotor: Julien Brunel, advisor: Virginie Wiels)


Collaborative projects

  • FORMEDICIS (ANR), MOISE (IRT Saint-Exupéry), TRUST (FCT, Portugal)
  • Formerly: Topcased (DGE/FUI), SPaCIFY (ANR), Cesar (Artemis), IMAP (DPAC), Merge (ITEA2), Cx (DGA & ANR)


  • ENSEEIHT: free software, software & law


Personal interests

  • Free software
  • Lacan, Freud, Foucault, psychoanalysis, structuralism, epistemology, history of ideas

Short vitæ

  • 2017: habilitation from Université Paul Sabatier
  • 2008-...: computer scientist at ONERA
  • 2004-2008: flight-software architect (Pléiades HR), in charge of R&T on methods and tools for critical-software engineering, and free-software specialist, at the French Space Agency (CNES)
  • 2000-2004: PhD (on type theory and rewriting) with Sergei Soloviev (advisor) at IRIT, and teaching assistant at Université Paul Sabatier
  • 1999-2000: MSc (on typed actor-based functional programming) with Patrick Sallé, Marc Pantel and Fabien Dagnat at IRIT/ENSEEIHT
  • For fun: my academic genealogy


In preparation

C. Chareton, J. Brunel, and D. Chemouil. Strategic Reasoning for the Evaluation of the Assignment of Behavioral Goals to Agents. Submitted, 2016.

Journal articles

C. Chareton, J. Brunel, and D. Chemouil. A Logic with Revocable and Refinable Strategies. Information and Computation (I&C), 242:157–182, 2015.
DOI | http | .pdf ]

D. Chemouil. An insertion operator preserving infinite reduction sequences. Mathematical Structures in Computer Science (MSCS), 18(4), 2008.
DOI | http | .pdf ]

D. Chemouil. Isomorphisms of simple inductive types through extensional rewriting. Mathematical Structures in Computer Science (MSCS), 15(5), 2005.
DOI | http ]

International conference/workshop articles

N. Macedo, J. Brunel, D. Chemouil, A. Cunha, and D. Kuperberg. Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. In Proc. ACM SIGSOFT Intl Symp. on the Foundations of Software Engineering (FSE), Seattle, United States, Nov. 2016.
http | .pdf ]

D. Kuperberg, J. Brunel, and D. Chemouil. On Finite Domains in First-Order Linear Temporal Logic. In 14th Interl Symp. on Automated Technology for Verification and Analysis (ATVA), Chiba, Japan, Oct. 2016. Long version.
DOI | http | .pdf ]

J. Brunel and D. Chemouil. Safety and Security Assessment of Behavioral Properties Using Alloy. In 2nd Intl workshop on the Integration of Safety and Security Engineering (ISSE), Delft, Netherlands, Sept. 2015.
http | .pdf ]

C. Chareton, J. Brunel, and D. Chemouil. Evaluating the Assignment of Behavioral Goals to Coalitions of Agents. In Brazilian Symp. on Formal Methods, Belo Horizonte, Brazil, Sept. 2015.
http | .pdf ]

J. Brunel, D. Chemouil, L. Rioux, M. Bakkali, and F. Vallée. A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures. In Proc. of the 11th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa) co-located with 17th Intl Conf. on Model Driven Engineering Languages and Systems (MODELS 2014), volume 1235. CEUR-WS, Sept. 2014.
http | .pdf ]

C. Chareton, J. Brunel, and D. Chemouil. Towards an Updatable Strategy Logic. In Proc. 1st Intl Workshop on Strategic Reasoning (SR), 2013.
DOI | http ]

S. Bouveret, J. Brunel, D. Chemouil, and F. Dagnat. Towards a categorical framework to ensure correct software evolutions. In HoTSWUp'11 (IEEE 27th Intl Conf. on Data Engineering Workshops), 2011.
DOI | http | .pdf ]

C. Chareton, J. Brunel, and D. Chemouil. A Formal Treatment of Agents, Goals and Operations Using Alternating-Time Temporal Logic. In Brazilian Symp. on Formal Methods (SBMF), 2011.
DOI | http | .pdf ]

J.-P. Bodeveix, D. Chemouil, M. Filali, and D. Thomas. Modes in Asynchronous Systems. In 13th IEEE Intl Conf. on Engineering of Complex Computer Systems (ICECCS), 2008.
DOI | http ]

R. Bedin França, J.-P. Bodeveix, D. Chemouil, M. Filali, J.-F. Rolland, and D. Thomas. The AADL behaviour annex – experiments and roadmap. In 12th IEEE Intl Conf. on Engineering of Complex Computer Systems (ICECCS), 2007.
DOI | http ]

J.-P. Bodeveix, R. Cavallero, D. Chemouil, M. Filali, and J.-F. Rolland. A mapping from AADL to Java-RTSJ. In Proc. of the 5th Intl workshop on Java technologies for real-time and embedded systems (JTRES), 2007.
DOI | http ]

J.-P. Bodeveix, D. Chemouil, M. Filali, and M. Strecker. Towards formalising AADL in Proof Assistants. In Proc. of the Second Intl Workshop on Formal Foundations of Embedded Software and Component-based Software Architectures (FESCA), volume 141, 2005.
DOI | http ]

S. Soloviev and D. Chemouil. Some Algebraic Structures in Lambda-Calculus with Inductive Types. In Types for Proofs and Programs (TYPES), 2004.
DOI | http ]

D. Chemouil and S. Soloviev. Remarks on isomorphisms of simple inductive types. In Mathematics, Logic and Computation (in honor of N.G. de Bruijn's 85th birthday), satellite event of ICALP, volume 85, 2003.
DOI | http ]

National conference/workshop articles

C. Chareton, J. Brunel, and D. Chemouil. Vers une sémantique des jeux pour un langage d'ingénierie des exigences par buts et agents. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2012.
http | .pdf ]

M. Piriquito, P. Bieber, J. Brunel, and D. Chemouil. Une vue sûreté de fonctionnement pour la vérification d'architectures abstraites. In Actes de la conférence francophone sur les architectures logicielles (CAL), 2012.
http | .pdf ]

F. Barral, D. Chemouil, and S. Soloviev. Non-Standard Reductions and Categorical Models in Typed Lambda-Calculus. Логические исследования (Logical Investigations), (12):300–315, 2005.
.pdf ]

Keynotes or lectures

D. Chemouil. The Design of Spacecraft On-Board Software. In Formal Specification and Development in B (Proc . Intl B Conference), page 3, 2007. Invited keynote.

D. Chemouil. The Design of Space Systems. In From MDD concepts to experiments and illustrations, Models driven engineering for distributed real-time embedded systems (MDD4DRES summer school), 2006.

Industrial publications, posters, etc.

J. Brunel, D. Chemouil, N. Mélédo, and V. Ibanez. Formal Modelling and Safety Analysis of an Avionic Functional Architecture with Alloy. In Embedded Real Time Software and Systems (ERTSS), Toulouse, France, 2014.
.pdf ]

P. Arberet, J. Bodeveix, F. Boniol, J. Buisson, G. Cannenterre, D. Chemouil, A. Cortier, F. Dagnat, F. Dupont, M. Filali, E. Fleury, G. Garcia, F. Herbreteau, E. Morand, J. Ouy, G. Sutre, A. Rugina, and M. Streker. SPaCIFY: a Formal Model-Driven Engineering for Spacecraft On-Board Software. In Embedded Real Time Software and Systems (ERTSS), 2010.
.pdf ]

D. Chemouil. The SPaCIFY Project. In Data Systems In Aerospace (DASIA), 2008.

J.-F. Rolland, M. Filali, J.-P. Bodeveix, D. Chemouil, D. Thomas, and A. Rossignol. AADL modes for space software. In Data Systems In Aerospace (DASIA), 2008.

J.-F. Rolland, J.-P. Bodeveix, D. Chemouil, M. Filali, and D. Thomas. Towards a formal semantics for AADL execution model. In Embedded Real-Time Software (ERTS), Toulouse, 2008.

D. Sabatier, B. Dellandrea, and D. Chemouil. FDIR Strategy Validation with the B method. In Data Systems In Aerospace (DASIA), 2008.

N. Pontisso and D. Chemouil. Vérification formelle d'un modèle AADL à l'aide de l'outil UPPAAL. Génie Logiciel, 80:36–40, 2007.

J.-F. Rolland, D. Thomas, and D. Chemouil. Utilisation d'AADL pour la conception de logiciels de vol satellite. Génie Logiciel, 80:41–44, 2007.

J.-P. Bodeveix, D. Chemouil, M. Filali, N. Lalevée, and M. Strecker. Towards the verification of model transformations. In Embedded Real-Time Software (ERTS). Société des Ingénieurs de l'Automobile, 2006.
http ]

J.-P. Bodeveix, M. Filali, M. Rached, D. Chemouil, and P. Gaufillet. Experimenting an AADL behavioural annex and a verification method. In Data Systems In Aerospace (DASIA), 2006.

F. Vernadat, C. Percebois, P. Farail, R. Vingerhoeds, A. Rossignol, J. P. Talpin, and D. Chemouil. The TOPCASED project-a toolkit in open-source for critical applications and system development. In Data Systems In Aerospace (DASIA), 2006.

N. Pontisso and D. Chemouil. TOPCASED Combining Formal Methods with Model-Driven Engineering. In Intl Conf on Automated Software Engineering ASE, pages 359–360, 2006. Poster.