A Parallel Prolog Execution Model Theoretical Approach and Experimental Results. - Jean-Paul Bodeveix; Érick Bizouarn (IPPS, 1993)

Towards a HOL Theory and Memory. - Jean-Paul Bodeveix; Mamoun Filali; P. Roche (TPHOLs, 1994)

On the Refinement of symmetric memory protocols. - Jean-Paul Bodeveix; Mamoun Filali (TPHOLs, 1995)

Towards the Automatic Verification of Atomic Memory Protocols. - Jean-Paul Bodeveix; Mamoun Filali (Parallel Process. Lett., 1997)

On the Automatic Validation of Parameterized Unity Programs. - Jean-Paul Bodeveix; Mamoun Filali (IPPS/SPDP Workshops, 1998)

Types versus classes. - Didier Plaindoux; Jean-Paul Bodeveix; Christian Percebois (Obj. Logiciel Base données Réseaux, 1998)

A Concurrent Object-Based Model and its Use for Coordinating Java Components. - Salam Majoul; Christian Percebois; Jean-Paul Bodeveix (TOOLS (30), 1999)

Experimenting Acceleration Methods for the Validation of Infinite State Systems. - Jean-Paul Bodeveix; Mamoun Filali (ICDCS Workshop on Distributed System Validation and Verification, 2000)

FMona: A Tool for Expressing Validation Techniques over Infinite State Systems. - Jean-Paul Bodeveix; Mamoun Filali (TACAS, 2000)

Abstract machine construction through operational semantics refinements. - Frédéric Cabestre; Christian Percebois; Jean-Paul Bodeveix (Future Gener. Comput. Syst., 2000)

Type Synthesis in B and the Translation of B to PVS. - Jean-Paul Bodeveix; Mamoun Filali (ZB, 2002)

Reduction and Quantifier Elimination Techniques for Program Validation. - Jean-Paul Bodeveix; Mamoun Filali (Formal Methods Syst. Des., 2002)

Vérification de modèles UML fondée sur OCL. - Pierre Bazex; Jean-Paul Bodeveix; Thierry Millan; Christophe Le Camus; Christian Percebois (INFORSID, 2003)

Towards the verification of real-time systems in avionics: the Cotre approach. - Bernard Berthomieu; Pierre-Olivier Ribet; François Vernadat 001; J. L. Bernartt; Jean-Marie Farines; Jean-Paul Bodeveix; Mamoun Filali; Gérard Padiou; Pierre Michel; Patrick Farail; Pierre Gauffilet; Pierre Dissaux; et al. (FMICS, 2003)

TransM: A Structured Document Transformation Model. - Nouhad Amaneddine; Jean Paul Bahsoun; Jean-Paul Bodeveix (ISTA, 2004)

Formal Methods Meet Domain Specific Languages. - Jean-Paul Bodeveix; Mamoun Filali; Julia Lawall; Gilles Muller (IFM, 2005)

Towards formalising AADL in Proof Assistants. - Jean-Paul Bodeveix; David Chemouil; Mamoun Filali; Martin Strecker (FESCA@ETAPS, 2005)

A State/Event Temporal Deontic Logic. - Julien Brunel; Jean-Paul Bodeveix; Mamoun Filali (DEON, 2006)

Verification of a scheduler in B through a timed automata specification. - Odile Nasr; Jean-Paul Bodeveix; Mamoun Filali; Miloud Rached Irit (SAC, 2006)

Automatic Verification of Bossa Scheduler Properties. - Jean-Paul Bodeveix; Mamoun Filali; Julia L. Lawall; Gilles Muller (AVoCS, 2006)

Security policy compliance with violation management. - Julien Brunel; Frédéric Cuppens; Nora Cuppens-Boulahia; Thierry Sans; Jean-Paul Bodeveix (FMSE, 2007)

The AADL behaviour annex - experiments and roadmap. - Ricardo Bedin França; Jean-Paul Bodeveix; Mamoun Filali; Jean-François Rolland; David Chemouil; Dave Thomas (ICECCS, 2007)

A mapping from AADL to Java-RTSJ. - Jean-Paul Bodeveix; Raphaël Cavallero; David Chemouil; Mamoun Filali; Jean-François Rolland (JTRES, 2007)

Modes in Asynchronous Systems. - Jean-François Rolland; Jean-Paul Bodeveix; Mamoun Filali; David Chemouil; Dave Thomas (ICECCS, 2008)

Spécification et vérification d'un ordonnanceur en B via les automates temporisés. - Odile Nasr; M. Rached; Jean-Paul Bodeveix; Mamoun Filali (Obj. Logiciel Base données Réseaux, 2008)

Formal Verification of AADL Specifications in the Topcased Environment. - Bernard Berthomieu; Jean-Paul Bodeveix; Christelle Chaudet; Silvano Dal-Zilio; Mamoun Filali; François Vernadat 001 (Ada-Europe, 2009)

Modeling AADL Data Communication with BIP. - Lei Pi; Jean-Paul Bodeveix; Mamoun Filali (Ada-Europe, 2009)

A Comparative Study of FIACRE and TASM to Define AADL Real Time Concepts. - Lei Pi; Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali; Kai Hu 004; Dianfu Ma (ICECCS, 2009)

Towards Safe Design of Synchronous Bus Protocols in Event-B. - Ricardo Bedin França; Leandro Buss Becker; Jean-Paul Bodeveix; Jean-Marie Farines; Mamoun Filali (SBMF, 2009)

Polychronous Interpretation of Synoptic, a Domain Specific Modeling Language for Embedded Flight-Software - Loïc Besnard; Thierry Gautier; Julien Ouy; Jean-Pierre Talpin; Jean-Paul Bodeveix; Alexandre Cortier; Marc Pantel; Martin Strecker; Gérald Garcia; Ana-Elena Rugina; Jérémy Buisson; Fabien Dagnat (FMA, 2009)

Synoptic: A Domain-Specific Modeling Language for Space On-board Application Software. - Alexandre Cortier; Loïc Besnard; Jean-Paul Bodeveix; Jérémy Buisson; Fabien Dagnat; Mamoun Filali; Gérald Garcia; Julien Ouy; Marc Pantel; Ana-Elena Rugina; Martin Strecker; Jean-Pierre Talpin (Synthesis of Embedded Software, 2010)

Supporting the Design of Safety Critical Systems Using AADL. - T. Correa; Leandro Buss Becker; Jean-Marie Farines; Jean-Paul Bodeveix; Mamoun Filali; François Vernadat 001 (ICECCS, 2010)

An Alternative Definition for Timed Automata Composition. - Jean-Paul Bodeveix; Abdeldjalil Boudjadar; Mamoun Filali (ATVA, 2011)

Verification of Timed BPEL 2.0 Models. - Elie Fares; Jean-Paul Bodeveix; Mamoun Filali (BMMDS/EMMSAD, 2011)

Two Formal Semantics of a Subset of the AADL. - Zhibin Yang; Kai Hu 004; Jean-Paul Bodeveix; Lei Pi; Dianfu Ma; Jean-Pierre Talpin (ICECCS, 2011)

Design of a BPEL Verification Tool. - Elie Fares; Jean-Paul Bodeveix; Mamoun Filali (WS-FM, 2011)

Event B Development of a Synchronous AADL Scheduler. - Jean-Paul Bodeveix; Mamoun Filali (B@FM, 2011)

Revising and Extending the Uppaal Communication Mechanism. - Abdeldjalil Boudjadar; Jean-Paul Bodeveix; Mamoun Filali (SC@TOOLS, 2012)

Compositional Refinement for Real-Time Systems with Priorities. - Abdeldjalil Boudjadar; Jean-Paul Bodeveix; Mamoun Filali (TIME, 2012)

An Automatic Technique for Checking the Simulation of Timed Systems. - Elie Fares; Jean-Paul Bodeveix; Mamoun Filali-Amine; Manuel Garnacho (ATVA, 2013)

A Mechanized Semantic Framework for Real-Time Systems. - Manuel Garnacho; Jean-Paul Bodeveix; Mamoun Filali-Amine (FORMATS, 2013)

Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems. - Abdeldjalil Boudjadar; Frits W. Vaandrager; Jean-Paul Bodeveix; Mamoun Filali (FSEN, 2013)

A comparative study of two formal semantics of the SIGNAL language. - Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali (Frontiers Comput. Sci., 2013)

Multi-Core Code Generation from Polychronous Programs with Time-Predictable Properties. - Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali (ACVI@MoDELS, 2014)

A verified transformation: from polychronous programs to a variant of clocked guarded actions. - Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali; Kai Hu 004; Dianfu Ma (SCOPES, 2014)

From AADL to Timed Abstract State Machines: A verified model transformation. - Zhibin Yang; Kai Hu 004; Dianfu Ma; Jean-Paul Bodeveix; Lei Pi; Jean-Pierre Talpin (J. Syst. Softw., 2014)

Real-Time Model Checking Support for AADL. - Bernard Berthomieu; Jean-Paul Bodeveix; Silvano Dal-Zilio; Mamoun Filali; Didier Le Botlan; Guillaume Verdier; François Vernadat 001 (CoRR, 2015)

Towards a verified transformation from AADL to the formal component-based language FIACRE. - Jean-Paul Bodeveix; Mamoun Filali; Manuel Garnacho; Régis Spadotti; Zhibin Yang (Sci. Comput. Program., 2015)

An Event-B Development Process for the Distributed BIP Framework. - Badr Siala; Mohamed Tahar Bhiri; Jean-Paul Bodeveix; Mamoun Filali (ICFEM, 2016)

Towards a verified compiler prototype for the synchronous language SIGNAL. - Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali; Kai Hu 004; Yongwang Zhao; Dianfu Ma (Frontiers Comput. Sci., 2016)

A refinement-based compiler development for synchronous languages. - Jean-Paul Bodeveix; Mamoun Filali-Amine; Shuanglong Kan (MEMOCODE, 2017)

Automatic Refinement for Event-B through Annotated Patterns. - Badr Siala; Jean-Paul Bodeveix; Mamoun Filali; Mohamed Tahar Bhiri (PDP, 2017)

An Event-B framework for the validation of Event-B refinement plugins. - Jean-Paul Bodeveix; Mamoun Filali; Mohamed Tahar Bhiri; Badr Siala (CoRR, 2017)

Hierarchical Behavior Annex: Towards an AADL Functional Specification Extension. - Jinmiao Xu; Zhibin Yang; Zhiqiu Huang; Yong Zhou; Chengwei Liu; Lei Xue; Jean-Paul Bodeveix; Mamoun Filali (MEMOCODE, 2018)

Event algebra for transition systems composition application to timed automata. - Elie Fares; Jean-Paul Bodeveix; Mamoun Filali (Acta Informatica, 2018)

Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol. - Jean-Paul Bodeveix; Julien Brunel; David Chemouil; Mamoun Filali (FM, 2019)

Automated Ada Code Generation from Synchronous Dataflow Programs on Multicore: Approach and Industrial Study. - Shenghao Yuan; Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali; Tiexin Wang; Yong Zhou (FTSCS, 2019)

A Formal Methods Approach to Security Requirements Specification and Verification. - Quentin Rouland; Brahim Hamid; Jean-Paul Bodeveix; Mamoun Filali (ICECCS, 2019)

Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL. - Zhibin Yang; Jean-Paul Bodeveix; Mamoun Filali (Frontiers Comput. Sci., 2019)

Formal Verification of Solidity contracts in Event-B. - Jian Zhu; Kai Hu 004; Mamoun Filali; Jean-Paul Bodeveix; Jean-Pierre Talpin (CoRR, 2020)

Event-B formalization of a variability-aware component model patterns framework. - Jean-Paul Bodeveix; Arnaud Dieumegard; Mamoun Filali (Sci. Comput. Program., 2020)

An Approach to Generate the Traceability Between Restricted Natural Language Requirements and AADL Models. - Fei Wang 049; Zhibin Yang; Zhi-qiu Huang; Chengwei Liu; Yong Zhou; Jean-Paul Bodeveix; Mamoun Filali (IEEE Trans. Reliab., 2020)

Event-B Formalization of Event-B Contexts. - Jean-Paul Bodeveix; Mamoun Filali (ABZ, 2021)

Sound Verification Procedures for Temporal Properties of Infinite-State Systems. - Quentin Peyras; Jean-Paul Bodeveix; Julien Brunel; David Chemouil (CAV (2), 2021)

Formal Simulation and Verification of Solidity contracts in Event-B. - Jian Zhu; Kai Hu 004; Mamoun Filali; Jean-Paul Bodeveix; Jean-Pierre Talpin; Haitao Cao 005 (COMPSAC, 2021)

Exploiting augmented intelligence in the modeling of safety-critical autonomous systems. - Zhibin Yang; Yang Bao 007; Yongqiang Yang; Zhiqiu Huang; Jean-Paul Bodeveix; Mamoun Filali; Zonghua Gu 001 (Formal Aspects Comput., 2021)

C2AADL_Reverse: A model-driven reverse engineering approach to development and verification of safety-critical software. - Zhibin Yang; Zhikai Qiu; Yong Zhou; Zhiqiu Huang; Jean-Paul Bodeveix; Mamoun Filali (J. Syst. Archit., 2021)

Multi-task Ada code generation from synchronous dataflow programs on multi-core: Approach and industrial study. - Zhibin Yang; Shenghao Yuan; Jean-Paul Bodeveix; Mamoun Filali; Tiexin Wang; Yong Zhou (Sci. Comput. Program., 2021)

Specification and Verification of Communication Paradigms for CBSE in Event B. - Loïc Thierry; Jason Jaskolka; Brahim Hamid; Jean-Paul Bodeveix (ICECCS, 2023)

Formalizing the Relationship between Security Policies and Objectives in Software Architectures. - Quentin Rouland; Brahim Hamid; Jean-Paul Bodeveix; Jason Jaskolka (ICSA-C, 2023)

Pattern-Based Refinement Generation Through Domain Specific Languages. - Elie Fares; Jean-Paul Bodeveix; Mamoun Filali (ABZ, 2023)

Correct Pattern-Based Development Through Refinements and Weakest Preconditions Calculus. - Elie Fares; Jean-Paul Bodeveix; Mamoun Filali (FACS, 2024)

Verifying HyperLTL Properties in Event-B. - Jean-Paul Bodeveix; Thomas Carle; Elie Fares; Mamoun Filali; Thai Son Hoang (ABZ, 2024)

Translating Event-B Models and Development Proofs to TLA+. - Anne Grieu; Jean-Paul Bodeveix; Mamoun Filali (ABZ, 2025)