Two Approaches towards the Formalisation of VDM. - Christine Lafontaine; Yves Ledru; Pierre-Yves Schobbens (VDM Europe, 1990)

Applying VDM to large developments. - Yves Ledru; Pierre-Yves Schobbens (Formal Methods in Software Development, 1990)

An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study. - Christine Lafontaine; Yves Ledru; Pierre-Yves Schobbens (Commun. ACM, 1991)

Prototyping VDM specifications with KIDS. - Yves Ledru; Marie-Hélène Liégeois (KBSE, 1992)

Developing Reactive Systems in a VDM Framework. - Yves Ledru (Sci. Comput. Program., 1993)

Proof-Based Development of Specifications with KIDS/VDM. - Yves Ledru (FME, 1994)

Environment-based Development of Reactive Systems. - Yves Ledru; Pierre Collette (Refine, 1994)

A VDM Specification of the Steam-Boiler Problem. - Yves Ledru; Marie-Laure Potet (Formal Methods for Industrial Applications, 1995)

Specification and Animation of a Bank Transfer. - Yves Ledru (KBSE, 1995)

Using KIDS as a Tool Support for VDM. - Yves Ledru (ICSE, 1996)

Complementing semi-formal specifications with Z. - Yves Ledru (KBSE, 1996)

Specification and Animation of a Bank Transfer using KIDS/VDM. - Yves Ledru (Autom. Softw. Eng., 1997)

Identifying Pre-Conditions with the Z/EVES Theorem Prover. - Yves Ledru (ASE, 1998)

Translating the OMT Dynamic Model into Object-Z. - Sophie Dupuy; Yves Ledru; Monique Chabre-Peccoud (ZUM, 1998)

Guest Editorial. - Christopher A. Welty; Michael R. Lowry; Yves Ledru (Autom. Softw. Eng., 1999)

An Overview of RoZ: A Tool for Integrating UML and Z Specifications. - Sophie Dupuy; Yves Ledru; Monique Chabre-Peccoud (CAiSE, 2000)

Vers une intégration utile de notations semi-formelles et formelles : une expérience en UML et Z. - Sophie Dupuy; Yves Ledru; Monique Chabre-Peccoud (Obj. Logiciel Base données Réseaux, 2000)

Helping Various Stakeholders to Understand a Very Large Component-Based Software. - Rémy Sanlaville; Jean-Marie Favre; Yves Ledru (EUROMICRO, 2001)

Test Purposes: Adapting the Notion of Specification to Testing. - Yves Ledru; Lydie du Bousquet; Pierre Bontron; Olivier Maury; Catherine Oriat; Marie-Laure Potet (ASE, 2001)

Report on the Workshop on the State of the Art in Automated Software Engineering. - Yves Ledru; David F. Redmiles (ASE, 2002)

Towards Computer-aided Design of OCL Constraints. - Yves Ledru; Sophie Dupuy-Chessa; Hind Fadil (CAiSE Workshops (1), 2004)

Filtering TOBIAS Combinatorial Test Suites. - Yves Ledru; Lydie du Bousquet; Olivier Maury; Pierre Bontron (FASE, 2004)

Case Study in JML-Based Software Validation. - Lydie du Bousquet; Yves Ledru; Olivier Maury; Catherine Oriat; Jean-Louis Lanet (ASE, 2004)

Object Oriented Concepts Identification from Formal B Specifications. - Akram Idani; Yves Ledru (FMICS, 2004)

Test of the ICARE Platform Fusion Mechanism. - Sophie Dupuy-Chessa; Lydie du Bousquet; Jullien Bouchet; Yves Ledru (DSV-IS, 2005)

Experiences in coverage testing of a Java middleware. - Mehdi Kessis; Yves Ledru; Gérard Vandome (SEM, 2005)

Derivation of UML Class Diagrams as Static Views of Formal B Developments. - Akram Idani; Yves Ledru; Didier Bert (ICFEM, 2005)

Validation of Regulation Documents by Automated Analysis of Formal Models. - Didier Bert; Fabrice Bouquet; Yves Ledru; Sylvie Vignes (ReMo2V, 2006)

A Formalisation of the Soccer Substitution Rules. - Yves Ledru (ReMo2V, 2006)

An attempt to combine UML and formal methods to model airport security. - Yves Ledru; Régine Laleau; Michel Lemoine; Sylvie Vignes; Didier Bert; Véronique Donzeau-Gouge; Catherine Dubois; Fabien Peureux (CAiSE Forum, 2006)

Tobias-Z: An executable formal specification of a test generator. - Yves Ledru; Lydie du Bousquet (ASE, 2006)

A Reverse-Engineering Approach to Understanding B Specifications with UML Diagrams. - Akram Idani; Yves Ledru; Didier Bert (SEW, 2006)

Using Jaza to Animate RoZ Specifications of UML Class Diagrams. - Yves Ledru (SEW, 2006)

Dynamic graphical UML views from formal B specifications. - Akram Idani; Yves Ledru (Inf. Softw. Technol., 2006)

Adopting a situational requirements engineering approach for the analysis of civil aviation security standards. - Régine Laleau; Sylvie Vignes; Yves Ledru; Michel Lemoine; Didier Bert; Véronique Donzeau-Gouge; Catherine Dubois; Fabien Peureux (Softw. Process. Improv. Pract., 2006)

Mastering combinatorial explosion with the tobias-2 test generator. - Yves Ledru; Frédéric Dadeau; Lydie du Bousquet; Sébastien Ville; Elodie Rose (ASE, 2007)

Using Computer Science Modeling Techniques for Airport Security Certification. - Régine Laleau; Yves Ledru; Didier Bert; Fabrice Bouquet; Michel Lemoine; Catherine Dubois; Véronique Donzeau-Gouge; Sylvie Vignes (RCIS, 2007)

Measuring a Java Test Suite Coverage Using JML Specifications. - Frédéric Dadeau; Yves Ledru; Lydie du Bousquet (MBT, 2007)

A Case Study in Matching Test and Proof Coverage. - Yves Ledru; Lydie du Bousquet; Frédéric Dadeau; F. Allouti (MBT, 2007)

Approche formelle pour la dérivation de vues structurelles UML à partir de développements B. Formalisation, preuve et extension pour la prise en compte des raffinements B. - Akram Idani; Yves Ledru; Didier Bert (Tech. Sci. Informatiques, 2007)

Une tentative d'utilisation conjointe d'UML et d'une méthode formelle pour la modélisation de la sécurité des aéroports. - Yves Ledru; Régine Laleau; Sylvie Vignes (Ingénierie des Systèmes d Inf., 2008)

Ingénierie Dirigée par les Modèles pour une intégration efficace de UML et B. - Akram Idani; Yves Ledru; Mohamed-Amine Labiadh (INFORSID, 2009)

Using String Distances for Test Case Prioritisation. - Yves Ledru; Alexandre Petrenko; Sergiy Boroday (ASE, 2009)

Assertion-based test oracles for home automation systems. - Ajitha Rajan; Lydie du Bousquet; Yves Ledru; Germán Vega; Jean-Luc Richier (MOMPES, 2010)

Infrastructure dirigée par les modèles pour une intégration adaptable et évolutive de UML et B. - Akram Idani; Mohamed-Amine Labiadh; Yves Ledru (Ingénierie des Systèmes d Inf., 2010)

Reusing a JML Specification Dedicated to Verification for Testing, and Vice-Versa: Case Studies. - Lydie du Bousquet; Yves Ledru; Olivier Maury; Catherine Oriat; Jean-Louis Lanet (J. Autom. Reason., 2010)

Evaluating RBAC Supported Techniques and their Validation and Verification. - Nafees Qamar; Yves Ledru; Akram Idani (ARES, 2011)

Taking into Account Functional Models in the Validation of IS Security Policies. - Yves Ledru; Akram Idani; Jérémy Milhau; Nafees Qamar; Régine Laleau; Jean-Luc Richier; Mohamed-Amine Labiadh (CAiSE Workshops, 2011)

Validation of Security-Design Models Using Z. - Nafees Qamar; Yves Ledru; Akram Idani (ICFEM, 2011)

Validation of security policies by the animation of Z specifications. - Yves Ledru; Nafees Qamar; Akram Idani; Jean-Luc Richier; Mohamed-Amine Labiadh (SACMAT, 2011)

Combining UML, ASTD and B for the formal specification of an access control filter. - Jérémy Milhau; Akram Idani; Régine Laleau; Mohamed-Amine Labiadh; Yves Ledru; Marc Frappier (Innov. Syst. Softw. Eng., 2011)

Model-Based Filtering of Combinatorial Test Suites. - Taha Triki; Yves Ledru; Lydie du Bousquet; Frédéric Dadeau; Julien Botella (FASE, 2012)

Automated Reviewing of Healthcare Security Policies. - Nafees Qamar; Johannes Faber; Yves Ledru; Zhiming Liu 001 (FHIES, 2012)

Test suite selection based on traceability annotations. - Yves Ledru; Germán Vega; Taha Triki; Lydie du Bousquet (ASE, 2012)

Prioritizing test cases with string distances. - Yves Ledru; Alexandre Petrenko; Sergiy Boroday; Nadine Mandran (Autom. Softw. Eng., 2012)

Apport d'un prototype spécifié en Z dans le redéveloppement d'un outil de test. - Yves Ledru; Lydie du Bousquet (Tech. Sci. Informatiques, 2012)

A Rigorous Reasoning about Model Transformations Using the B Method. - Akram Idani; Yves Ledru; Adil Anwar (BMMDS/EMMSAD, 2013)

Test Generation and Evaluation from High-Level Properties for Common Criteria Evaluations - The TASCCC Testing Tool. - Frédéric Dadeau; Kalou Cabrera Castillos; Yves Ledru; Taha Triki; Germán Vega; Julien Botella; Safouan Taha (ICST, 2013)

Extraction of Insider Attack Scenarios from a Formal Information System Modeling. - Amira Radhouani; Akram Idani; Yves Ledru; Narjes Ben Rajeb (FMS @ Petri Nets, 2014)

B Formal Validation of ERTMS/ETCS Railway Operating Rules. - Rahma Ben Ayed; Simon Collart Dutilleul; Philippe Bon; Akram Idani; Yves Ledru (ABZ, 2014)

Modélisation graphique et validation formelle de politiques RBAC en systèmes d'information. Plateforme B4MSecure. - Akram Idani; Yves Ledru; Amira Radhouani (Ingénierie des Systèmes d Inf., 2014)

B for Modeling Secure Information Systems - The B4MSecure Platform. - Akram Idani; Yves Ledru (ICFEM, 2015)

Validation of a Security Policy by the Test of Its Formal B Specification - A Case Study. - Yves Ledru; Akram Idani; Jean-Luc Richier (FormaliSE@ICSE, 2015)

Extensions du diagramme d'activité pour contrôler l'accès au SI. - Salim Chehida; Akram Idani; Yves Ledru; Mustapha Kamel Rahmouni (INFORSID, 2015)

Validation of IS Security Policies Featuring Authorisation Constraints. - Yves Ledru; Akram Idani; Jérémy Milhau; Nafees Qamar; Régine Laleau; Jean-Luc Richier; Mohamed-Amine Labiadh (Int. J. Inf. Syst. Model. Des., 2015)

Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling. - Amira Radhouani; Akram Idani; Yves Ledru; Narjes Ben Rajeb (Trans. Petri Nets Other Model. Concurr., 2015)

Formalismes basés sur les rôles pour la modélisation et la validation des règles d'exploitation ferroviaires. - Rahma Ben Ayed; Simon Collart Dutilleul; Philippe Bon; Yves Ledru; Akram Idani (Tech. Sci. Informatiques, 2015)

Combining UML and B for the specification and validation of RBAC policies in business process activities. - Salim Chehida; Akram Idani; Yves Ledru; Mustapha Kamel Rahmouni (RCIS, 2016)

Extensions du diagramme d'activité pour la spécification de politiques RBAC. - Salim Chehida; Akram Idani; Yves Ledru; Mustapha Kamel Rahmouni (Ingénierie des Systèmes d Inf., 2016)

Improving Trace Generation and Analysis for Medical Devices. - Yoann Blein; Arnaud Clere; Fabrice Bertrand; Yves Ledru; Roland Groz; Lydie du Bousquet (QRS Companion, 2017)

Extending specification patterns for verification of parametric traces. - Yoann Blein; Yves Ledru; Lydie du Bousquet; Roland Groz (FormaliSE@ICSE, 2018)

Requirements for a Trace Property Language for Medical Devices. - Yves Ledru; Yoann Blein; Lydie du Bousquet; Roland Groz; Arnaud Clere; Fabrice Bertrand (SEHS@ICSE, 2018)

Formalizing Railway Signaling System ERTMS/ETCS Using UML/Event-B. - Abderrahim Ait Wakrime; Rahma Ben Ayed; Simon Collart Dutilleul; Yves Ledru; Akram Idani (MEDI, 2018)

An Environment for the ParTraP Trace Property Language (Tool Demonstration). - Ansem Ben Cheikh; Yoann Blein; Salim Chehida; Germán Vega; Yves Ledru; Lydie du Bousquet (RV, 2018)

Incremental Development of a Safety Critical System Combining formal Methods and DSMLs - - Application to a Railway System -. - Akram Idani; Yves Ledru; Abderrahim Ait Wakrime; Rahma Ben Ayed; Simon Collart Dutilleul (FMICS, 2019)

Towards a Tool-Based Domain Specific Approach for Railway Systems Modeling and Validation. - Akram Idani; Yves Ledru; Abderrahim Ait Wakrime; Rahma Ben Ayed; Philippe Bon (RSSRail, 2019)

A Separation of Concerns Approach for the Verified Modelling of Railway Signalling Rules. - Yves Ledru; Akram Idani; Rahma Ben Ayed; Abderrahim Ait Wakrime; Philippe Bon (RSSRail, 2019)

Reducing Regression Test Suites using the Word2Vec Natural Language Processing Tool. - Bahareh Afshinpour; Roland Groz; Massih-Reza Amini; Yves Ledru; Catherine Oriat (SEED/NLPaSE@APSEC, 2020)

Alliance of model-driven engineering with a proof-based formal approach. - Akram Idani; Yves Ledru; Germán Vega (Innov. Syst. Softw. Eng., 2020)

An SMT-based approach for generating trace examples and counter-examples of parametric properties. - Salim Chehida; Yves Ledru; Yoann Blein; Germán Vega (Int. J. Crit. Comput. Based Syst., 2021)

Visual animation of B specifications using executable DSLs. - Asfand Yar; Akram Idani; Yves Ledru; Simon Collart Dutilleul (MoDELS (Companion), 2022)

A Process-Centric Approach to Insider Threats Identification in Information Systems. - Akram Idani; Yves Ledru; Germán Vega (CRiSIS, 2023)

DroidSecTester: Towards context-driven modelling and detection of Android application vulnerabilities. - Ivan Baheux; Oum-El-Kheir Aktouf; Mohammed El Amin Tebib; Mariem Graa; Pascal André; Yves Ledru (ISSREW, 2023)

An Iterative Formal Model-Driven Approach to Railway Systems Validation. - Asfand Yar; Akram Idani; Yves Ledru; Simon Collart Dutilleul; Amel Mammar; Germán Vega (ICECCS, 2024)

Formal model-driven security combining B-method and process algebra. - Akram Idani; Yves Ledru; Germán Vega (Innov. Syst. Softw. Eng., 2025)