| 2026 | FM | Specializing Anti-unification for Interaction Models Composition via Gate Connections. | Joel Nguetoum, Boutheina Bannour, Pascale Le Gall, Erwan Mahe |
| 2025 | LOPSTR | Program Synthesis for Geometric Modeling. | Romain Pascual, Pascale Le Gall, Hakim Belhaouari, Agns Arnould |
| 2024 | ISoLA | High-Level Program Properties in Frama-C: Definition, Verification and Deduction. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall |
| 2022 | IFM | Certified Verification of Relational Properties. | Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall |
| 2022 | ISoLA | An Efficient VCGen-Based Modular Verification of Relational Properties. | Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall |
| 2022 | TASE | Equivalence of Denotational and Operational Semantics for Interaction Languages. | Erwan Mahe, Christophe Gaston, Pascale Le Gall |
| 2021 | ICSE | Methodology for Specification and Verification of High-Level Requirements with MetAcsl. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall |
| 2021 | MEDI | Deriving Interaction Scenarios for Timed Distributed Systems by Symbolic Execution. | Boutheina Bannour, Arnault Lapitre, Pascale Le Gall |
| 2021 | SAC | A small-step approach to multi-trace checking against interactions. | Erwan Mahe, Boutheina Bannour, Christophe Gaston, Arnault Lapitre, Pascale Le Gall |
| 2020 | FASE | Revisiting Semantics of Interactions for Trace Validity Analysis. | Erwan Mahe, Christophe Gaston, Pascale Le Gall |
| 2019 | ICST | Behavioral Models and Scenario Selection for Testing IoT Trickle-Based Lossy Multicast Networks. | Ngo Minh Thang Nguyen, Boutheina Bannour, Arnault Lapitre, Pascale Le Gall |
| 2019 | TACAS | MetAcsl: Specification and Verification of High-Level Properties. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall |
| 2019 | TAP | Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. | Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall |
| 2018 | FASE | Fast Computation of Arbitrary Control Dependencies. | Jean-Christophe Lchenet, Nikolai Kosmatov, Pascale Le Gall |
| 2018 | TAP | Static and Dynamic Verification of Relational Properties on Self-composed C Code. | Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot |
| 2017 | TACAS | RPP: Automatic Proof of Relational Properties by Self-composition. | Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto |
| 2017 | TAP | Symbolic Execution of Transition Systems with Function Summaries. | Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto |
| 2016 | FASE | Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices. | Jean-Christophe Lchenet, Nikolai Kosmatov, Pascale Le Gall |
| 2016 | ISORC | Timed-Model-Based Method for Security Analysis and Testing of Smart Grid Systems. | Gabriel Pedroza, Pascale Le Gall, Christophe Gaston, Fabrice Bersey |
| 2014 | APSEC | Security Weaknesses Detection by Symbolic Analysis of Scenarios. | Boutheina Bannour, Jose Pablo Escobedo, Christophe Gaston, Pascale Le Gall, Gabriel Pedroza |
| 2014 | ICFEM | An LTL Model Checking Approach for Biological Parameter Inference. | Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall, Paolo Ballarini |
| 2014 | ICST | Designing Sequence Diagram Models for Robustness to Attacks. | Boutheina Bannour, Jose Pablo Escobedo, Christophe Gaston, Pascale Le Gall, Gabriel Pedroza |
| 2014 | ISoLA | Formal Analysis of the Wnt/β-catenin through Statistical Model Checking. | Paolo Ballarini, Emmanuelle Gallet, Pascale Le Gall, Matthieu Manceny |
| 2010 | SEFM | Testing Web Service Orchestrators in Context: A Symbolic Approach. | Jose Pablo Escobedo, Christophe Gaston, Pascale Le Gall, Ana R. Cavalli |
| 2008 | APSEC | Emergent Properties in Reactive Systems. | Marc Aiguier, Pascale Le Gall, Mbarka Mabrouki |
| 2008 | ICSEA | A Formal Definition of Complex Software. | Marc Aiguier, Pascale Le Gall, Mbarka Mabrouki |
| 2008 | ICST | Generation of All-Paths Unit Test with Function Calls. | Patricia Mouy, Bruno Marre, Nicky Williams, Pascale Le Gall |
| 2007 | LATA | Topology-based Geometric Modelling for Biological Cellular Processes. | Mathieu Poudret, Jean-Paul Comet, Pascale Le Gall, Agns Arnould, Philippe Meseure |
| 2007 | TAP | Symbolic Execution Techniques for Refinement Testing. | Pascale Le Gall, Nicolas Rapin, Assia Touil |
| 2006 | FM | Feature Specification and Static Analysis for Interaction Resolution. | Marc Aiguier, Karim Berkani, Pascale Le Gall |
| 2005 | APSEC | A Temporal Logic for Input Output Symbolic Transition Systems. | Marc Aiguier, Pascale Le Gall, Delphine Longuet, Assia Touil |
| 2002 | APSEC | Feature Logics and Refinement. | Marc Aiguier, Christophe Gaston, Pascale Le Gall |
| 1997 | ICSE | A Theory of Probabilistic Functional Testing. | Gilles Bernot, Laurent Bouaziz, Pascale Le Gall |
| 1996 | EDCC | Dynamic Testing from Bounded Data Type Specifications. | Agns Arnould, Pascale Le Gall, Bruno Marre |
| 1995 | COMPASS | Formal Specifications and Test: Correctness and Oracle. | Pascale Le Gall, Agns Arnould |
| 1991 | COMPASS | Label Algebras: A Systematic Use of Terms. | Gilles Bernot, Pascale Le Gall |