David Chemouil

David Chemouil - Homepage
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


  • 05/2018: Presentation of Electrum at the MIT workshop on the Future of Alloy .
  • 01/2018: The all-new versions of our free-software tools around the Electrum language are released (collaboration with A. Cunha and N. Macedo): cf.  Electrum Analyzer and Electrod repositories
  • 01/2018: PC and organization of the FMIS 2018, the 7th International Workshop on Formal Methods for Interactive Systems, affiliated to STAF 2018.
  • 12/2017: two PhD propositions: one on the 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.


See my PUBLICATIONS below (you may also visit DBLP and HAL, many thanks to them)

Current topics

  • My main research purpose is to build bridges between theoretical computer science and software engineering.
  • At the moment, I mainly work on the foundational and more applied aspects Electrum, an extension of Alloy with temporal logic.
  • Former research interests include: isomorphisms of types; formal methods for critical embedded software; multi-agent temporal logic for goal- and agent-oriented requirements modeling.
  • I'm a fan of Alloy and OCaml.
  • 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), Alcino Cunha (U. Braga), Nuno Macedo (U. Braga), Denis Kuperberg (ENS Lyon), Mamoun Filali (IRIT), Jean-Paul Bodeveix (IRIT)

PhD students and Postdoctoral researchers


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


Collaborative projects

  • FORMEDICIS (ANR), MOISE (IRT Saint-Exupéry), TRUST (FCT, Portugal), IFSE2 (Fondation STAE)
  • Formerly: Topcased (DGE/FUI), SPaCIFY (ANR), Cesar (Artemis), IMAP (DPAC), Merge (ITEA2), Briefcase (RTRA STAE), 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 ]

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 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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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, 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 ]

Short papers

J. Brunel, D. Chemouil, A. Cunha, T. Hujsa, N. Macedo, and J. Tawa. Proposition of an Action Layer for Electrum. In 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, Southampton, United Kingdom, June 2018.
http | .pdf ]

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.

National conference/workshop articles

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 ]

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 ]

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. Sabatier, B. Dellandrea, and D. Chemouil. FDIR Strategy Validation with the B method. 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.

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.

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

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.

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.

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.

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.

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 ]