CADP - A Protocol Validation and Verification Toolbox. - Jean-Claude Fernandez; Hubert Garavel; Alain Kerbrat; Laurent Mounier; Radu Mateescu 001; Mihaela Sighireanu (CAV, 1996)

Verification of Temporal Properties of Processes in a Setting with Data. - Jan Friso Groote; Radu Mateescu 001 (AMAST, 1998)

Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): An Experiment with E-LOTOS. - Mihaela Sighireanu; Radu Mateescu 001 (Int. J. Softw. Tools Technol. Transf., 1998)

Vérification des propriétés temporelles des programmes parallèles. (Verification of temporal properties of parallel programs). - Radu Mateescu 001 (1998)

Model Checking for Managers. - Wil Janssen; Radu Mateescu 001; Sjouke Mauw; Peter Fennema; Petra van der Stappen (SPIN, 1999)

Efficient Diagnostic Generation for Boolean Equation Systems. - Radu Mateescu 001 (TACAS, 2000)

Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. - Manuel Aguilar Cornejo; Hubert Garavel; Radu Mateescu 001; Noel De Palma (DAIS, 2001)

Parallel State Space Construction for Model-Checking. - Hubert Garavel; Radu Mateescu 001; Irina M. Smarandache (SPIN, 2001)

Compiler Construction Using LOTOS NT. - Hubert Garavel; Frédéric Lang; Radu Mateescu 001 (CC, 2002)

Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. - Radu Mateescu 001 (TACAS, 2002)

Calculating-Confluence Compositionally. - Gordon J. Pace; Frédéric Lang; Radu Mateescu 001 (CAV, 2003)

A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. - Radu Mateescu 001 (TACAS, 2003)

On-the-Fly Verification using CADP. - Radu Mateescu 001 (FMICS, 2003)

Efficient on-the-fly model-checking for regular alternation-free mu-calculus. - Radu Mateescu 001; Mihaela Sighireanu (Sci. Comput. Program., 2003)

Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones. - Radu Mateescu 001 (Tech. Sci. Informatiques, 2003)

Model Checking for Software Architectures. - Radu Mateescu 001 (EWSA, 2004)

Model Checking Genetic Regulatory Networks Using GNA and CADP. - Grégory Batt; Damien Bergamini; Hidde de Jong; Hubert Garavel; Radu Mateescu 001 (SPIN, 2004)

SEQ.OPEN: A Tool for Efficient Trace-Based Verification. - Hubert Garavel; Radu Mateescu 001 (SPIN, 2004)

A Generic Framework for Model Checking Software Architectures. - Radu Mateescu 001 (VVEIS, 2004)

Distributed On-the-Fly Equivalence Checking. - Christophe Joubert; Radu Mateescu 001 (PDMC, 2004)

On-the-fly state space reductions for weak equivalences. - Radu Mateescu 001 (FMICS, 2005)

Analysis and Verification of Qualitative Models of Genetic Regulatory Networks: A Model-Checking Approach. - Grégory Batt; Delphine Ropers; Hidde de Jong; Johannes Geiselmann; Radu Mateescu 001; Michel Page; Dominique Schneider (IJCAI, 2005)

Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli. - Grégory Batt; Delphine Ropers; Hidde de Jong; Johannes Geiselmann; Radu Mateescu 001; Michel Page; Dominique Schneider (ISMB (Supplement of Bioinformatics), 2005)

Distributed Local Resolution of Boolean Equation Systems. - Christophe Joubert; Radu Mateescu 001 (PDP, 2005)

BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. - Damien Bergamini; Nicolas Descoubes; Christophe Joubert; Radu Mateescu 001 (TACAS, 2005)

Distributed On-the-Fly Model Checking and Test Case Generation. - Christophe Joubert; Radu Mateescu 001 (SPIN, 2006)

DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. - Hubert Garavel; Radu Mateescu 001; Damien Bergamini; Adrian Curic; Nicolas Descoubes; Christophe Joubert; Irina Smarandache-Sturm; Gilles Stragier (TACAS, 2006)

pi-AAL: an architecture analysis language for formally specifying and verifying structural and behavioural properties of software architectures. - Radu Mateescu 001; Flávio Oquendo (ACM SIGSOFT Softw. Eng. Notes, 2006)

CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems. - Radu Mateescu 001 (Int. J. Softw. Tools Technol. Transf., 2006)

CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. - Hubert Garavel; Radu Mateescu 001; Frédéric Lang; Wendelin Serwe (CAV, 2007)

Behavioral adaptation of component compositions based on process algebra encodings. - Radu Mateescu 001; Pascal Poizat; Gwen Salaün (ASE, 2007)

Computation Tree Regular Logic for Genetic Regulatory Networks. - Radu Mateescu 001; Pedro T. Monteiro 001; Estelle Dumas; Hidde de Jong (ATVA, 2008)

Formal Modeling and Discrete-Time Analysis of BPEL Web Services. - Radu Mateescu 001; Sylvain Rampacek (CIAO! / EOMAS, 2008)

Temporal Logic Patterns for Querying Qualitative Models of Genetic Regulatory Networks. - Pedro T. Monteiro 001; Delphine Ropers; Radu Mateescu 001; Ana T. Freitas; Hidde de Jong (ECAI, 2008)

Temporal logic patterns for querying dynamic models of cellular interaction networks. - Pedro T. Monteiro 001; Delphine Ropers; Radu Mateescu 001; Ana T. Freitas; Hidde de Jong (ECCB, 2008)

A Model Checking Language for Concurrent Value-Passing Systems. - Radu Mateescu 001; Damien Thivolle (FM, 2008)

Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems. - Radu Mateescu 001; Emilie Oudot (MEMOCODE, 2008)

Improved On-the-Fly Equivalence Checking Using Boolean Equation Systems. - Radu Mateescu 001; Emilie Oudot (SPIN, 2008)

Formal modelling and discrete-time analysis of BPEL web services. - Radu Mateescu 001; Sylvain Rampacek (Int. J. Simul. Process. Model., 2008)

Modeling Multiprocessor Cache Protocol Impact on MPI Performance. - Ghassan Chehaibar; Meriem Zidouni; Radu Mateescu 001 (AINA Workshops, 2009)

Partial Order Reductions Using Compositional Confluence Detection. - Frédéric Lang; Radu Mateescu 001 (FM, 2009)

Hierarchical Adaptive State Space Caching Based on Level Sampling. - Radu Mateescu 001; Anton Wijs (TACAS, 2009)

A service-oriented architecture for integrating the modeling and formal verification of genetic regulatory networks. - Pedro T. Monteiro 001; Estelle Dumas; Bruno Besson; Radu Mateescu 001; Michel Page; Ana T. Freitas; Hidde de Jong (BMC Bioinform., 2009)

Modeling and formal verification of biological regulatory networks: An integrative approach. - Pedro T. Monteiro 001; Ana T. Freitas; Delphine Ropers; Radu Mateescu 001; Hidde de Jong (BIBM Workshops, 2010)

A Study of Shared-Memory Mutual Exclusion Protocols Using CADP. - Radu Mateescu 001; Wendelin Serwe (FMICS, 2010)

Translating Pi-Calculus into LOTOS NT. - Radu Mateescu 001; Gwen Salaün (IFM, 2010)

Ten Years of Performance Evaluation for Concurrent Systems Using CADP. - Nicolas Coste; Hubert Garavel; Holger Hermanns; Frédéric Lang; Radu Mateescu 001; Wendelin Serwe (ISoLA (2), 2010)

Property-Dependent Reductions for the Modal Mu-Calculus. - Radu Mateescu 001; Anton Wijs (SPIN, 2011)

CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. - Hubert Garavel; Frédéric Lang; Radu Mateescu 001; Wendelin Serwe (TACAS, 2011)

CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. - Radu Mateescu 001; Pedro T. Monteiro 001; Estelle Dumas; Hidde de Jong (Theor. Comput. Sci., 2011)

Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems. - Frédéric Lang; Radu Mateescu 001 (TACAS, 2012)

Large-scale Distributed Verification Using CADP: Beyond Clusters to Grids. - Hubert Garavel; Radu Mateescu 001; Wendelin Serwe (PASM/PDMC, 2012)

Sequential and distributed on-the-fly computation of weak tau-confluence. - Radu Mateescu 001; Anton Wijs (Sci. Comput. Program., 2012)

Adaptation of Service Protocols Using Process Algebra and On-the-Fly Reduction Techniques. - Radu Mateescu 001; Pascal Poizat; Gwen Salaün (IEEE Trans. Software Eng., 2012)

PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. - Radu Mateescu 001; Gwen Salaün (TACAS, 2013)

Composition and abstraction of logical regulatory modules: application to multicellular systems. - Nuno D. Mendes; Frédéric Lang; Yves-Stan Le Cornec; Radu Mateescu 001; Grégory Batt; Claudine Chaouiya (Bioinform., 2013)

Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems. - Frédéric Lang; Radu Mateescu 001 (Log. Methods Comput. Sci., 2013)

Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. - Radu Mateescu 001; Wendelin Serwe (Sci. Comput. Program., 2013)

CADP 2011: a toolbox for the construction and analysis of distributed processes. - Hubert Garavel; Frédéric Lang; Radu Mateescu 001; Wendelin Serwe (Int. J. Softw. Tools Technol. Transf., 2013)

Quantifying the parallelism in BPMN processes using model checking. - Radu Mateescu 001; Gwen Salaün; Lina Ye (CBSE, 2014)

GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems. - Fatma Jebali; Frédéric Lang; Radu Mateescu 001 (ICFEM, 2014)

Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. - Radu Mateescu 001; Anton Wijs (Sci. Comput. Program., 2014)

Compositional verification of asynchronous concurrent systems using CADP. - Hubert Garavel; Frédéric Lang; Radu Mateescu 001 (Acta Informatica, 2015)

Formal modelling and verification of GALS systems using GRL and CADP. - Fatma Jebali; Frédéric Lang; Radu Mateescu 001 (Formal Aspects Comput., 2016)

Verification of EB3 specifications using CADP. - Dimitris Vekris; Frédéric Lang; Catalin Dima; Radu Mateescu 001 (Formal Aspects Comput., 2016)

The ContextAct@A4H Real-Life Dataset of Daily-Living Activities - Activity Recognition Using Model Checking. - Paula Lago; Frédéric Lang; Claudia Roncancio; Claudia Jiménez-Guarín; Radu Mateescu 001; Nicolas Bonnefond (CONTEXT, 2017)

Model-Checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits. - Aymane Bouzafour; Marc Renaudin; Hubert Garavel; Radu Mateescu 001; Wendelin Serwe (ASYNC, 2018)

Reflections on Bernhard Steffen's Physics of Software Tools. - Hubert Garavel; Radu Mateescu 001 (Models, Mindsets, Meta, 2018)

Using LNT Formal Descriptions for Model-Based Diagnosis. - Birgit Hofer; Radu Mateescu 001; Wendelin Serwe; Franz Wotawa (DX, 2018)

TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation. - Lina Marsso; Radu Mateescu 001; Wendelin Serwe (TACAS (2), 2018)

A Formal TLS Handshake Model in LNT. - Josip Bozic; Lina Marsso; Radu Mateescu 001; Franz Wotawa (MARS/VPT@ETAPS, 2018)

Recent advances in interactive and automated analysis. - Radu Mateescu 001 (Int. J. Softw. Tools Technol. Transf., 2018)

On-the-fly model checking for extended action-based probabilistic operators. - Radu Mateescu 001; José Ignacio Requeno (Int. J. Softw. Tools Technol. Transf., 2018)

Hunting Superfluous Locks with Model Checking. - Viet-Anh Nguyen; Wendelin Serwe; Radu Mateescu 001; Eric Jenn (From Software Engineering to Formal Methods and Tools, and Back, 2019)

Rigorous design and deployment of IoT applications. - Ajay Krishna 001; Michel Le Pallec; Radu Mateescu 001; Ludovic Noirie; Gwen Salaün (FormaliSE@ICSE, 2019)

IoT composer: composition and deployment of IoT applications. - Ajay Krishna 001; Michel Le Pallec; Radu Mateescu 001; Ludovic Noirie; Gwen Salaün (ICSE (Companion Volume), 2019)

Asynchronous Testing of Synchronous Components in GALS Systems. - Lina Marsso; Radu Mateescu 001; Ioannis Parissis; Wendelin Serwe (IFM, 2019)

Formal Validation of Probabilistic Collision Risk Estimation for Autonomous Driving. - Philippe Ledent; Anshul Paigwar; Alessandro Renzaglia; Radu Mateescu 001; Christian Laugier (CIS/RAM, 2019)

Automated Transition Coverage in Behavioural Conformance Testing. - Lina Marsso; Radu Mateescu 001; Wendelin Serwe (ICTSS, 2020)

Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities. - Frédéric Lang; Radu Mateescu 001; Franco Mazzanti (TACAS (2), 2020)

MOZART: Design and Deployment of Advanced IoT Applications. - Ajay Krishna 001; Michel Le Pallec; Alejandro Martinez; Radu Mateescu 001; Gwen Salaün (WWW (Companion Volume), 2020)

Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks. - Radu Mateescu 001; Wendelin Serwe; Aymane Bouzafour; Marc Renaudin (MARS@ETAPS, 2020)

R-MOZART: A Reconfiguration Tool for WebThings Applications. - Francisco Durán 001; Ajay Krishna 001; Michel Le Pallec; Radu Mateescu 001; Gwen Salaün (ICSE (Companion Volume), 2021)

Seamless Reconfiguration of Rule-based IoT Applications. - Francisco Durán 001; Ajay Krishna 001; Michel Le Pallec; Radu Mateescu 001; Gwen Salaün (SEAMS@ICSE, 2021)

Is CADP an Applicable Formal Method? - Hubert Garavel; Frédéric Lang; Radu Mateescu 001; Wendelin Serwe (AppFM@FM, 2021)

Compositional verification of concurrent systems by combining bisimulations. - Frédéric Lang; Radu Mateescu 001; Franco Mazzanti (Formal Methods Syst. Des., 2021)

Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles. - Jean-Baptiste Horel; Christian Laugier; Lina Marsso; Radu Mateescu 001; Lucie Muller; Anshul Paigwar; Alessandro Renzaglia; Wendelin Serwe (DATE, 2022)

Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing. - Lina Marsso; Radu Mateescu 001; Lucie Muller; Wendelin Serwe (MARS@ETAPS, 2022)

Models and analysis for user-driven reconfiguration of rule-based IoT applications. - Francisco Durán 001; Ajay Krishna 001; Michel Le Pallec; Radu Mateescu 001; Gwen Salaün (Internet Things, 2022)

Design and Deployment of Expressive and Correct Web of Things Applications. - Ajay Krishna 001; Michel Le Pallec; Radu Mateescu 001; Gwen Salaün (ACM Trans. Internet Things, 2022)

Verifying Collision Risk Estimation using Autonomous Driving Scenarios Derived from a Formal Model. - Jean-Baptiste Horel; Philippe Ledent; Lina Marsso; Lucie Muller; Christian Laugier; Radu Mateescu 001; Anshul Paigwar; Alessandro Renzaglia; Wendelin Serwe (J. Intell. Robotic Syst., 2023)

Improving PSS Test Generation Using Model Checking and Conformance Testing. - Philippe Ledent; Radu Mateescu 001; Wendelin Serwe (FDL, 2024)

Testing Resource Isolation for System-on-Chip Architectures. - Philippe Ledent; Radu Mateescu 001; Wendelin Serwe (MARS@ETAPS, 2024)