Model Checking with Edge-valued Decision Diagrams. - Pierre Roux 001; Radu Siminiceanu (NASA Formal Methods, 2010)

SMT-AI: an Abstract Interpreter as Oracle for k-induction. - Pierre Roux 001; Remi Delmas; Pierre-Loïc Garoche (TAPAS@SAS, 2010)

A generic ellipsoid abstract domain for linear time invariant systems. - Pierre Roux 001; Romain Jobredeaux; Pierre-Loïc Garoche; Eric Feron (HSCC, 2012)

Integrating Policy Iterations in Abstract Interpreters. - Pierre Roux 001; Pierre-Loïc Garoche (ATVA, 2013)

Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses. - Adrien Champion; Rémi Delmas; Michael Dierkes; Pierre-Loïc Garoche; Romain Jobredeaux; Pierre Roux 001 (FMICS, 2013)

Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison. - Pierre Roux 001; Pierre-Loïc Garoche (FM, 2014)

Innocuous Double Rounding of Basic Arithmetic Operations. - Pierre Roux 001 (J. Formaliz. Reason., 2014)

Closed loop analysis of control command software. - Pierre Roux 001; Romain Jobredeaux; Pierre-Loïc Garoche (HSCC, 2015)

Practical policy iterations - A practical use of policy iterations for static analysis: the quadratic case. - Pierre Roux 001; Pierre-Loïc Garoche (Formal Methods Syst. Des., 2015)

Embedding network calculus and event stream theory in a common model. - Marc Boyer; Pierre Roux 001 (ETFA, 2016)

Formal Analysis of Robustness at Model and Code Level. - Timothy E. Wang; Pierre-Loïc Garoche; Pierre Roux 001; Romain Jobredeaux; Eric Feron (HSCC, 2016)

Formal Proofs of Rounding Error Bounds - With Application to an Automatic Positive Definiteness Check. - Pierre Roux 001 (J. Autom. Reason., 2016)

A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. - Érik Martin-Dorel; Pierre Roux 001 (CPP, 2017)

Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code. - Guillaume Davy; Christophe Garion; Pierre-Loïc Garoche; Pierre Roux 001; Xavier Thirioux (FDL, 2018)

A Non-linear Arithmetic Procedure for Control-Command Software Verification. - Pierre Roux 001; Mohamed Iguernlala; Sylvain Conchon (TACAS (2), 2018)

Validating numerical semidefinite programming solvers for polynomial invariants. - Pierre Roux 001; Yuen-Lam Voronin; Sriram Sankaranarayanan 001 (Formal Methods Syst. Des., 2018)

Primitive Floats in Coq. - Guillaume Bertholon; Érik Martin-Dorel; Pierre Roux 001 (ITP, 2019)

A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus. - Marc Boyer; Pierre Roux 001; Hugo Daigmorte; David Puechmaille (ECRTS, 2021)

Verifying the Mathematical Library of an UAV Autopilot with Frama-C. - Baptiste Pollien; Christophe Garion; Gautier Hattenberger; Pierre Roux 001; Xavier Thirioux (FMICS, 2021)

Verifying Min-Plus Computations with Coq. - Lucien Rakotomalala; Pierre Roux 001; Marc Boyer (NFM, 2021)

A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact). - Marc Boyer; Pierre Roux 001; Hugo Daigmorte; David Puechmaille (Dagstuhl Artifacts Ser., 2021)

A Formal Link Between Response Time Analysis and Network Calculus. - Pierre Roux 001; Sophie Quinton; Marc Boyer (ECRTS, 2022)

A Formal Link Between Response Time Analysis and Network Calculus (Artifact). - Pierre Roux 001; Sophie Quinton; Marc Boyer (Dagstuhl Artifacts Ser., 2022)

A Verified UAV Flight Plan Generator. - Baptiste Pollien; Christophe Garion; Gautier Hattenberger; Pierre Roux 001; Xavier Thirioux (FormaliSE, 2023)

CTA: A Correlation-Tolerant Analysis of the Deadline-Failure Probability of Dependent Tasks. - Filip Markovic 001; Pierre Roux 001; Sergey Bozhko; Alessandro V. Papadopoulos; Björn B. Brandenburg (RTSS, 2023)

Enabling Floating-Point Arithmetic in the Coq Proof Assistant. - Érik Martin-Dorel; Guillaume Melquiond; Pierre Roux 001 (J. Autom. Reason., 2023)