4 Search Results for "Roux, Cody"

Document

DOI: 10.4230/LIPIcs.ITP.2024.14

End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation

Authors: Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of the proof makes it way too costly in practice. This article revisits the issue by proposing a methodology and some dedicated automation, and applies them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modeling of an external code; it is an actual floating-point function defined in the logic of the Coq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20× speedup with respect to the previous implementation.

Cite as

Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond. End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{faissole_et_al:LIPIcs.ITP.2024.14,
  author =	{Faissole, Florian and Geneau de Lamarli\`{e}re, Paul and Melquiond, Guillaume},
  title =	{{End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.14},
  URN =		{urn:nbn:de:0030-drops-207420},
  doi =		{10.4230/LIPIcs.ITP.2024.14},
  annote =	{Keywords: Program verification, floating-point arithmetic, formal proof, automated reasoning, mathematical library}
}

Document

DOI: 10.4230/LIPIcs.ITP.2024.31

A Verified Earley Parser

Authors: Martin Rau and Tobias Nipkow

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

An Earley parser is a top-down parsing technique that is capable of parsing arbitrary context-free grammars. We present a functional implementation of an Earley parser verified using the interactive theorem prover Isabelle/HOL. Our formalization builds upon Cliff Jones' extensive, refinement-based paper proof. We implement and prove soundness and completeness of a functional recognizer modeling Jay Earley’s original imperative implementation and extend it with the necessary data structures to enable the construction of parse trees following the work of Elizabeth Scott. Building upon this foundation, we develop a functional parser and prove its soundness. We round off the paper by providing an informal argument and empirical data regarding the running time and space complexity of our implementation.

Cite as

Martin Rau and Tobias Nipkow. A Verified Earley Parser. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{rau_et_al:LIPIcs.ITP.2024.31,
  author =	{Rau, Martin and Nipkow, Tobias},
  title =	{{A Verified Earley Parser}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{31:1--31:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.31},
  URN =		{urn:nbn:de:0030-drops-207596},
  doi =		{10.4230/LIPIcs.ITP.2024.31},
  annote =	{Keywords: Verification, Parsers, Earley, Isabelle}
}

Document

DOI: 10.4230/LIPIcs.ITP.2019.24

A Verified LL(1) Parser Generator

Authors: Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux

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

Abstract

An LL(1) parser is a recursive descent algorithm that uses a single token of lookahead to build a grammatical derivation for an input sequence. We present an LL(1) parser generator that, when applied to grammar G, produces an LL(1) parser for G if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete, and that they terminate on all inputs without using fuel parameters. As a case study, we extract the tool’s source code and use it to generate a JSON parser. The generated parser runs in linear time; it is two to four times slower than an unverified parser for the same grammar.

Cite as

Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux. A Verified LL(1) Parser Generator. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lasser_et_al:LIPIcs.ITP.2019.24,
  author =	{Lasser, Sam and Casinghino, Chris and Fisher, Kathleen and Roux, Cody},
  title =	{{A Verified LL(1) Parser Generator}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{24:1--24:18},
  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.24},
  URN =		{urn:nbn:de:0030-drops-110794},
  doi =		{10.4230/LIPIcs.ITP.2019.24},
  annote =	{Keywords: interactive theorem proving, top-down parsing}
}

Document

DOI: 10.4230/LIPIcs.RTA.2011.299

Refinement Types as Higher-Order Dependency Pairs

Authors: Cody Roux

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract

Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher-order rewrite systems is still the subject of active research. We observe that a variant of refinement types allows us to express a form of higher-order dependency pair method: from the rewrite system labeled with typing information, we build a type-level approximated dependency graph, and describe a type level embedding preorder. We describe a syntactic termination criterion involving the graph and the preorder, which generalizes the simple projection criterion of Middeldorp and Hirokawa, and prove our main result: if the graph passes the criterion, then every well-typed term is strongly normalizing.

Cite as

Cody Roux. Refinement Types as Higher-Order Dependency Pairs. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 299-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{roux:LIPIcs.RTA.2011.299,
  author =	{Roux, Cody},
  title =	{{Refinement Types as Higher-Order Dependency Pairs}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{299--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.299},
  URN =		{urn:nbn:de:0030-drops-31273},
  doi =		{10.4230/LIPIcs.RTA.2011.299},
  annote =	{Keywords: Dependency Pairs, Higher-Order, Refinement Types}
}

Refine by Author
2 Roux, Cody
1 Casinghino, Chris
1 Faissole, Florian
1 Fisher, Kathleen
1 Geneau de Lamarlière, Paul
Show More...

Refine by Classification
3 Software and its engineering → Formal software verification
2 Software and its engineering → Parsers
1 Mathematics of computing → Interval arithmetic
1 Mathematics of computing → Mathematical software performance
1 Theory of computation → Automated reasoning
Show More...

Refine by Keyword
1 Dependency Pairs
1 Earley
1 Higher-Order
1 Isabelle
1 Parsers
Show More...

Refine by Type
4 document

Refine by Publication Year
2 2024
1 2011
1 2019