Pierre Roux

28 papers A 1B 8C 4Journal 7Unranked 8
YearRankTypeTitle / Venue / Authors
2025 B conf
Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation.
ITP
Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa
2023 — conf
A Verified UAV Flight Plan Generator.
FormaliSE
Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux, Xavier Thirioux
2023 A conf
CTA: A Correlation-Tolerant Analysis of the Deadline-Failure Probability of Dependent Tasks.
RTSS
Filip Markovic, Pierre Roux, Sergey Bozhko, Alessandro V. Papadopoulos, Björn B. Brandenburg
2023 J jnl
Enabling Floating-Point Arithmetic in the Coq Proof Assistant.
J. Autom. Reason.
Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux
2022 J jnl
A Formal Link Between Response Time Analysis and Network Calculus (Artifact).
Dagstuhl Artifacts Ser.
Pierre Roux, Sophie Quinton, Marc Boyer
2022 B conf
A Formal Link Between Response Time Analysis and Network Calculus.
ECRTS
Pierre Roux, Sophie Quinton, Marc Boyer
2021 J jnl
A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact).
Dagstuhl Artifacts Ser.
Marc Boyer, Pierre Roux, Hugo Daigmorte, David Puechmaille
2021 B conf
A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus.
ECRTS
Marc Boyer, Pierre Roux, Hugo Daigmorte, David Puechmaille
2021 — conf
Verifying Min-Plus Computations with Coq.
NFM
Lucien Rakotomalala, Pierre Roux, Marc Boyer
2021 C conf
Verifying the Mathematical Library of an UAV Autopilot with Frama-C.
FMICS
Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux, Xavier Thirioux
2019 B conf
Primitive Floats in Coq.
ITP
Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux
2018 — conf
A Non-linear Arithmetic Procedure for Control-Command Software Verification.
TACAS (2)
Pierre Roux, Mohamed Iguernlala, Sylvain Conchon
2018 C conf
Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code.
FDL
Guillaume Davy, Christophe Garion, Pierre-Loïc Garoche, Pierre Roux, Xavier Thirioux
2018 J jnl
Validating numerical semidefinite programming solvers for polynomial invariants.
Formal Methods Syst. Des.
Pierre Roux, Yuen-Lam Voronin, Sriram Sankaranarayanan
2017 B conf
A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations.
CPP
Érik Martin-Dorel, Pierre Roux
2016 C conf
Embedding network calculus and event stream theory in a common model.
ETFA
Marc Boyer, Pierre Roux
2016 — conf
Formal Analysis of Robustness at Model and Code Level.
HSCC
Timothy E. Wang, Pierre-Loïc Garoche, Pierre Roux, Romain Jobredeaux, Eric Feron
2016 J jnl
Formal Proofs of Rounding Error Bounds - With Application to an Automatic Positive Definiteness Check.
J. Autom. Reason.
Pierre Roux
2016 B conf
Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants.
SAS
Pierre Roux, Yuen-Lam Voronin, Sriram Sankaranarayanan
2015 — conf
Closed loop analysis of control command software.
HSCC
Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche
2015 J jnl
Practical policy iterations - A practical use of policy iterations for static analysis: the quadratic case.
Formal Methods Syst. Des.
Pierre Roux, Pierre-Loïc Garoche
2014 B conf
Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison.
FM
Pierre Roux, Pierre-Loïc Garoche
2014 J jnl
Innocuous Double Rounding of Basic Arithmetic Operations.
J. Formaliz. Reason.
Pierre Roux
2013 C conf
Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses.
FMICS
Adrien Champion, Rémi Delmas, Michael Dierkes, Pierre-Loïc Garoche, Romain Jobredeaux, Pierre Roux
2013 B conf
Integrating Policy Iterations in Abstract Interpreters.
ATVA
Pierre Roux, Pierre-Loïc Garoche
2012 — conf
A generic ellipsoid abstract domain for linear time invariant systems.
HSCC
Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche, Eric Feron
2010 — conf
Model Checking with Edge-valued Decision Diagrams.
NASA Formal Methods
Pierre Roux, Radu Siminiceanu
2010 — conf
SMT-AI: an Abstract Interpreter as Oracle for k-induction.
TAPAS@SAS
Pierre Roux, Remi Delmas, Pierre-Loïc Garoche