David Chemouil

David Chemouil - Homepage
Picture of David Chemouil

David Chemouil
Senior Researcher, Computer Science (PhD, habil.)

2 avenue Édouard Belin, 31055  Toulouse, France

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





  • Current topics:
    • Foundational and applied aspects of the Electrum lightweight formal method (an extension of Alloy with LTL that I have co-authored).
    • Formal analysis of protocols, in particular the Chord DHT.
  • Free/open-source software: Electrum Analyzer, Electrod
  • Former interests include: isomorphisms of types; formal methods for critical embedded software; multi-agent temporal logic for goal- and agent-oriented requirements modeling, model-based safety & security assessment (MBSSA).
  • DBLP, HAL.


  • Member of the Alloy board
  • PC co-chair AFADL 2019
  • PC member FM 2019
  • PC member FMIS 2019
  • PC member and co-organizer FMIS 2018
  • PC member ABZ 2016
  • PC member CSDM 2010
  • Subreviewer for various conferences and workshops



  • Quentin Peyras (PhD student, co-promotor: J. Brunel)
  • External advisor for Chong Liu's PhD (advisors: A. Cunha & N. Macedo, U. Braga)


Collaborative projects

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


  • ENSEEIHT: advanced functional programming; free software
  • Formerly (Univ. Paul Sabatier, ENSEEIHT, ENAC, ISAE/SupAéro): universal algebra and algebraic specification, formal specification, computability theory, language theory and compilation techniques, imperative programming and axiomatic semantics, requirements engineering

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
  • Personal interests
    • Free software
    • Lacan, Freud, Foucault, psychoanalysis, structuralism, epistemology, history of ideas

Academic Publications

[29] Simulation under arbitrary temporal logic constraints. J. Brunel, D. Chemouil, A. Cunha & N. Macedo. In 5th Workshop on Formal Integrated Development Environment. Porto, Portugal, 2019. [ HAL open archive | PDF ]
[28] Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol. J.-P. Bodeveix, J. Brunel, D. Chemouil & M. Filali. In 23rd International Symposium on Formal Methods (FM 2019). Porto, Portugal, 2019. [ DOI | HAL open archive | PDF ]
[27] A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic. Q. Peyras, J. Brunel & D. Chemouil. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Málaga, Spain, 2019. [ DOI | HAL open archive | PDF ]
[26] Analyzing the Fundamental Liveness Property of the Chord Protocol. J. Tawa, J. Brunel & D. Chemouil. In Formal Methods in Computer-Aided Design (FMCAD). Austin, United States, 2018. [ DOI | HAL open archive | model | PDF ]
[25] The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications. J. Brunel, D. Chemouil, A. Cunha & N. Macedo. In 33rd ACM/IEEE Intl Conf on Automated Software Engineering (ASE). ACM Press, Montpellier, France, 2018. [ DOI | HAL open archive | PDF ]
[24] Proposition of an Action Layer for Electrum. J. Brunel, D. Chemouil, A. Cunha, T. Hujsa, N. Macedo & J. Tawa. In 6th Intl Conf on ASM, Alloy, B, TLA, VDM, Z (ABZ). Southampton, United Kingdom, 2018. [ DOI | HAL open archive | PDF ]
[23] Spécification légère et analyse de systèmes dynamiques munis de configurations riches. N. Macedo, J. Brunel, D. Chemouil, A. Cunha & D. Kuperberg. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). Montpellier, France, 2017. [ http | PDF ]
[22] Sur l'assignation de buts comportementaux à des coalitions d'agents. C. Chareton, J. Brunel & D. Chemouil. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). Montpellier, France, 2017. [ HAL open archive | PDF ]
[21] Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. N. Macedo, J. Brunel, D. Chemouil, A. Cunha & D. Kuperberg. In Proc. ACM SIGSOFT Intl Symp. on the Foundations of Software Engineering (FSE). Seattle, United States, 2016. [ DOI | HAL open archive | PDF ]
[20] On Finite Domains in First-Order Linear Temporal Logic. D. Kuperberg, J. Brunel & D. Chemouil. In 14th Intl Symp on Automated Technology for Verification and Analysis (ATVA). Chiba, Japan, 2016. Long version. [ DOI | HAL open archive | PDF ]
[19] Evaluating the Assignment of Behavioral Goals to Coalitions of Agents. C. Chareton, J. Brunel & D. Chemouil. In Brazilian Symp. on Formal Methods (SBMF). Belo Horizonte, Brazil, 2015. [ DOI | HAL open archive | PDF ]
[18] Safety and Security Assessment of Behavioral Properties Using Alloy. J. Brunel & D. Chemouil. In 2nd Intl workshop on the Integration of Safety and Security Engineering (ISSE). Delft, Netherlands, 2015. [ DOI | HAL open archive | PDF ]
[17] A Logic with Revocable and Refinable Strategies. C. Chareton, J. Brunel & D. Chemouil. Information and Computation (I&C), vol. 242:(2015) pp. 157–182. [ DOI | HAL open archive | PDF ]
[16] A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures. J. Brunel, D. Chemouil, L. Rioux, M. Bakkali & F. Vallée. 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), vol. 1235. CEUR-WS, 2014. [ HAL open archive | PDF ]
[15] Towards an Updatable Strategy Logic. C. Chareton, J. Brunel & D. Chemouil. In Proc. 1st Intl Workshop on Strategic Reasoning (SR). 2013. [ DOI | HAL open archive ]
[14] Une vue sûreté de fonctionnement pour la vérification d'architectures abstraites. M. Piriquito, P. Bieber, J. Brunel & D. Chemouil. In Conférence francophone sur les architectures logicielles (CAL). 2012. [ HAL open archive | PDF ]
[13] Vers une sémantique des jeux pour un langage d'ingénierie des exigences par buts et agents. C. Chareton, J. Brunel & D. Chemouil. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). 2012. [ HAL open archive | PDF ]
[12] A Formal Treatment of Agents, Goals and Operations Using Alternating-Time Temporal Logic. C. Chareton, J. Brunel & D. Chemouil. In Brazilian Symp. on Formal Methods (SBMF). 2011. [ DOI | HAL open archive | PDF ]
[11] Towards a categorical framework to ensure correct software evolutions. S. Bouveret, J. Brunel, D. Chemouil & F. Dagnat. In HoTSWUp'11 (IEEE 27th Intl Conf. on Data Engineering Workshops). 2011. [ DOI | HAL open archive | PDF ]
[10] An insertion operator preserving infinite reduction sequences. D. Chemouil. Mathematical Structures in Computer Science (MSCS), vol. 18(4). [ DOI | HAL open archive | PDF ]
[9] Modes in Asynchronous Systems. J.-P. Bodeveix, D. Chemouil, M. Filali & D. Thomas. In 13th IEEE Intl Conf. on Engineering of Complex Computer Systems (ICECCS). 2008. [ DOI | HAL open archive ]
[8] A mapping from AADL to Java-RTSJ. J.-P. Bodeveix, R. Cavallero, D. Chemouil, M. Filali & J.-F. Rolland. In Proc. of the 5th Intl workshop on Java technologies for real-time and embedded systems (JTRES). 2007. [ DOI | HAL open archive ]
[7] The AADL behaviour annex – experiments and roadmap. R. Bedin França, J.-P. Bodeveix, D. Chemouil, M. Filali, J.-F. Rolland & D. Thomas. In 12th IEEE Intl Conf. on Engineering of Complex Computer Systems (ICECCS). 2007. [ DOI | HAL open archive ]
[6] TOPCASED Combining Formal Methods with Model-Driven Engineering. N. Pontisso & D. Chemouil. In 21st IEEE/ACM Intl Conf on Automated Software Engineering ASE, pp. 359–360. 2006. Tool demo. [ DOI ]
[5] Isomorphisms of simple inductive types through extensional rewriting. D. Chemouil. Mathematical Structures in Computer Science (MSCS), vol. 15(5). [ DOI | HAL open archive ]
[4] Towards formalising AADL in Proof Assistants. J.-P. Bodeveix, D. Chemouil, M. Filali & M. Strecker. In Proc. of the Second Intl Workshop on Formal Foundations of Embedded Software and Component-based Software Architectures (FESCA), vol. 141. 2005. [ DOI | HAL open archive ]
[3] Non-Standard Reductions and Categorical Models in Typed Lambda-Calculus. F. Barral, D. Chemouil & S. Soloviev. Логические исследования (Logical Investigations), (12):(2005) pp. 300–315. [ PDF ]
[2] Some Algebraic Structures in Lambda-Calculus with Inductive Types. S. Soloviev & D. Chemouil. In Types for Proofs and Programs (TYPES). 2004. [ DOI | HAL open archive ]
[1] Remarks on isomorphisms of simple inductive types. D. Chemouil & S. Soloviev. In Mathematics, Logic and Computation (in honor of N.G. de Bruijn's 85th birthday), satellite event of ICALP, vol. 85. 2003. [ DOI | HAL open archive ]


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

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

Industrial Publications

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

SPaCIFY: a Formal Model-Driven Engineering for Spacecraft On-Board Software. 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. In Embedded Real Time Software and Systems (ERTSS), 2010.

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

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

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

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

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

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

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

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

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