David Chemouil

→ LINK TO PUBLICATIONS

Research

• Current topics:
  • Alloy (our own experiments go under the umbrella name "Electrum")
  • Formal specification and verification
  • Verification of distributed algorithms
  • Model-based safety assessment (MBSA)
• Free/open-source prototypes: Electrum Analyzer, Electrod, Cervino
• Former interests include: isomorphisms of types; formal methods for critical embedded software; multi-agent temporal logic for goal- and agent-oriented requirements modeling.
• DBLP, HAL.

Advising

• Quentin Peyras (PhD 2022, co-promotor: J. Brunel)
• External advisor for Chong Liu's PhD (PhD 2021, advisors: A. Cunha & N. Macedo, U. Braga)
• Jeanne Tawa (PhD 2019, co-advisor: J. Brunel): an action layer of Electrum and modelling of the Chord protocol
• Thomas Hujsa (postdoc 2018, co-advisor: J. Brunel)
• Denis Kuperberg (postdoc 2014-2015, co-promotors: Julien Brunel & Jean-Paul Bodeveix)
• Christophe Chareton (PhD 2014, co-promotor: Julien Brunel, advisor: Laurence Cholvy): formal requirements modelling and multi-agent temporal logics
• CNES advisor for the PhDs of Jean-François Rolland (2008, supervision: Jean-Paul Bodeveix & Mamoun Filali) and Nadège Pontisso (2009, supervision: Gérard Padiou & Philippe Queinnec)

Collaborative projects

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

Teaching

• ENSEEIHT: introduction to formal modelling (Coq, Why3); advanced functional programming in OCaml
• Formerly (Univ. Paul Sabatier, ENSEEIHT, ENAC, ISAE/SupAéro): formal specification of transition systems (TLA+/TLC), universal algebra and algebraic specification, formal specification, computability theory, language theory and compilation techniques, imperative programming and axiomatic semantics, requirements engineering, software law and free software

Short vitæ

• 2017: Habilitation from Université Paul Sabatier
• 2008-...: research 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 CNES, 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

[34]	Adding records to Alloy. J. Brunel, D. Chemouil, A. Cunha & N. Macedo. In 9th international conference on rigorous state-based methods. Springer Nature Switzerland, Nancy, France, 2023. [ DOI | HAL open archive | PDF ]
[33]	Verifying temporal relational models with Pardinus. J. Brunel, D. Chemouil, A. Cunha & N. Macedo. In 9th international conference on rigorous state-based methods. Springer Nature Switzerland, Nancy, France, 2023. [ DOI | HAL open archive | PDF ]
[32]	Pardinus: A temporal relational model finder. N. Macedo, J. Brunel, D. Chemouil & A. Cunha. Journal of Automated Reasoning, 2022. [ DOI | HAL open archive | PDF ]
[31]	Sound Verification Procedures for Temporal Properties of Infinite-State Systems. Q. Peyras, J.-P. Bodeveix, J. Brunel & D. Chemouil. In 33rd International Conference on Computer-Aided Verification (CAV 2021). Los Angeles (Online), United States, 2021. [ DOI | HAL open archive | artifact | PDF ]
[30]	A Decidable and Expressive Fragment of Many-Sorted First-Order Linear Temporal Logic. Q. Peyras, J. Brunel & D. Chemouil. Information and Computation, p. 104641, 2020. [ DOI | HAL open archive | PDF ]
[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 | artifact | 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. [ HAL open archive | 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, 2015. [ 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), 2008. [ 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), 2005. [ 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, 2005. [ 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 ]

Keynotes/Lectures

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.