Search Results

Documents authored by Roux, Pierre

Document
DOI: 10.4230/LIPIcs.ITP.2025.21
Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation

Authors: Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Concentration inequalities are standard lemmas providing upper bounds on deviations of random variables. To formalize concentration inequalities, we have been developing a general library of lemmas for probability theory in the Rocq prover. This effort led us to revisit already established technical aspects of the Mathematical Components libraries. In this paper, we report on improvements of general interest resulting from our formalization. We devise types for numeric values and a lightweight semi-decision procedure, based on interval arithmetic. We also extend the hierarchy of available mathematical structures to formalize Lebesgue spaces. We illustrate our new formalization of probability theory with the complete proof of a concentration inequality for Bernoulli sampling.
Cite as

Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa. Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2025.21,
  author =	{Affeldt, Reynald and Bruni, Alessandro and Cohen, Cyril and Roux, Pierre and Saikawa, Takafumi},
  title =	{{Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.21},
  URN =		{urn:nbn:de:0030-drops-246195},
  doi =		{10.4230/LIPIcs.ITP.2025.21},
  annote =	{Keywords: Rocq prover, Mathematical Components library, abstraction interpretation, probability theory, concentration inequalities}
}
Document
Artifact
DOI: 10.4230/DARTS.8.1.3
A Formal Link Between Response Time Analysis and Network Calculus (Artifact)

Authors: Pierre Roux, Sophie Quinton, and Marc Boyer

Published in: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)

Abstract
Classical Response Time Analysis (RTA) and Network Calculus (NC) are two major formalisms used for the verification of real-time properties. The related paper offer mathematical links between these two different theories. Based on these links, it then proves the equivalence of various key notions in both frameworks. This enables specialists of both formalisms to get increase confidence on their models, or even, like the authors, to discover errors in theorems by investigating apparent discrepancies between some notions expected to be equivalent. The presented mathematical results are all mechanically checked with the interactive theorem prover Coq, building on existing formalizations of RTA and NC. Establishing such a link between NC and RTA paves the way for improved real-time analyses obtained by combining both theories to enjoy their respective strengths (e.g., multicore analyses for RTA or clock drifts for NC). This artifact enables to reproduce these proofs.
Cite as

Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus (Artifact). In Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 1, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{roux_et_al:DARTS.8.1.3,
  author =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  title =	{{A Formal Link Between Response Time Analysis and Network Calculus (Artifact)}},
  pages =	{3:1--3:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{1},
  editor =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.1.3},
  URN =		{urn:nbn:de:0030-drops-164990},
  doi =		{10.4230/DARTS.8.1.3},
  annote =	{Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2022.5
A Formal Link Between Response Time Analysis and Network Calculus

Authors: Pierre Roux, Sophie Quinton, and Marc Boyer

Published in: LIPIcs, Volume 231, 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)

Abstract
Classical Response Time Analysis (RTA) and Network Calculus (NC) are two major formalisms used for the verification of real-time properties. We offer mathematical links between these two different theories. Based on these links, we then prove the equivalence of various key notions in both frameworks. This enables specialists of both formalisms to get increase confidence on their models, or even, like the authors, to discover errors in theorems by investigating apparent discrepancies between some notions expected to be equivalent. The presented mathematical results are all mechanically checked with the interactive theorem prover Coq, building on existing formalizations of RTA and NC. Establishing such a link between NC and RTA paves the way for improved real-time analyses obtained by combining both theories to enjoy their respective strengths (e.g., multicore analyses for RTA or clock drifts for NC).
Cite as

Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{roux_et_al:LIPIcs.ECRTS.2022.5,
  author =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  title =	{{A Formal Link Between Response Time Analysis and Network Calculus}},
  booktitle =	{34th Euromicro Conference on Real-Time Systems (ECRTS 2022)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-239-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{231},
  editor =	{Maggio, Martina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2022.5},
  URN =		{urn:nbn:de:0030-drops-163224},
  doi =		{10.4230/LIPIcs.ECRTS.2022.5},
  annote =	{Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq}
}
Document
Artifact
DOI: 10.4230/DARTS.7.1.2
A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact)

Authors: Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille

Published in: DARTS, Volume 7, Issue 1, Special Issue of the 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)

Abstract
Computing response times for resources shared by periodic workloads (tasks or data flows) can be very time consuming as it depends on the least common multiple of the periods. In a previous study, a quadratic algorithm was provided to upper bound the response time of a set of periodic tasks with a fixed-priority scheduling. The related paper generalises this result by considering a rate-latency server and sporadic workloads and gives a response time and residual curve that can be used in other contexts. It also provides a formal proof in the Coq language. This artifact enables to reproduce this proof.
Cite as

Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille. A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact). In Special Issue of the 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 1, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{boyer_et_al:DARTS.7.1.2,
  author =	{Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David},
  title =	{{A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{1},
  editor =	{Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.1.2},
  URN =		{urn:nbn:de:0030-drops-139810},
  doi =		{10.4230/DARTS.7.1.2},
  annote =	{Keywords: Network Calculus, response time, residual curve, rate-latency server, sporadic workload, formal proof, Coq}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2021.14
A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus

Authors: Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille

Published in: LIPIcs, Volume 196, 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)

Abstract
Computing response times for resources shared by periodic workloads (tasks or data flows) can be very time consuming as it depends on the least common multiple of the periods. In a previous study, a quadratic algorithm was provided to upper bound the response time of a set of periodic tasks with a fixed-priority scheduling. This paper generalises this result by considering a rate-latency server and sporadic workloads and gives a response time and residual curve that can be used in other contexts. It also provides a formal proof in the Coq language.
Cite as

Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille. A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus. In 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 196, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{boyer_et_al:LIPIcs.ECRTS.2021.14,
  author =	{Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David},
  title =	{{A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus}},
  booktitle =	{33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)},
  pages =	{14:1--14:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-192-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{196},
  editor =	{Brandenburg, Bj\"{o}rn B.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2021.14},
  URN =		{urn:nbn:de:0030-drops-139457},
  doi =		{10.4230/LIPIcs.ECRTS.2021.14},
  annote =	{Keywords: Network Calculus, response time, residual curve, rate-latency server, sporadic workload, formal proof, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.7
Primitive Floats in Coq

Authors: Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.
Cite as

Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux. Primitive Floats in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bertholon_et_al:LIPIcs.ITP.2019.7,
  author =	{Bertholon, Guillaume and Martin-Dorel, \'{E}rik and Roux, Pierre},
  title =	{{Primitive Floats in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.7},
  URN =		{urn:nbn:de:0030-drops-110629},
  doi =		{10.4230/LIPIcs.ITP.2019.7},
  annote =	{Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact