Allez au contenu, Allez à la navigation



David Chemouil

David Chemouil
Computer Scientist (Dr. habil.)
Picture of David Chemouil

2 avenue Édouard Belin
31055 Toulouse, France

Tel: +33 (0) 5 6225 2936
Fax: +33 (0) 5 6225 2593
ORCID: 0000-0003-4136-783X


  • 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.


Current topics

PUBLICATIONS (see also DBLP and HAL, many thanks to them)

  • 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)
  • Publications in industrial conferences

PhD students and Postdoctoral researchers


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


Collaborative projects

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


  • 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