Search Results

Documents authored by Darulova, Eva

Document
DOI: 10.4230/LIPIcs.ITP.2022.6
Dandelion: Certified Approximations of Elementary Functions

Authors: Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Elementary function operations such as sin and exp cannot in general be computed exactly on today’s digital computers, and thus have to be approximated. The standard approximations in library functions typically provide only a limited set of precisions, and are too inefficient for many applications. Polynomial approximations that are customized to a limited input domain and output accuracy can provide superior performance. In fact, the Remez algorithm computes the best possible approximation for a given polynomial degree, but has so far not been formally verified. This paper presents Dandelion, an automated certificate checker for polynomial approximations of elementary functions computed with Remez-like algorithms that is fully verified in the HOL4 theorem prover. Dandelion checks whether the difference between a polynomial approximation and its target reference elementary function remains below a given error bound for all inputs in a given constraint. By extracting a verified binary with the CakeML compiler, Dandelion can validate certificates within a reasonable time, fully automating previous manually verified approximations.
Cite as

Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ITP.2022.6,
  author =	{Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste},
  title =	{{Dandelion: Certified Approximations of Elementary Functions}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.6},
  URN =		{urn:nbn:de:0030-drops-167155},
  doi =		{10.4230/LIPIcs.ITP.2022.6},
  annote =	{Keywords: elementary functions, approximation, certificate checking}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.10
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)

Authors: Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the "fast-math-style" optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This document describes the artifact for RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
Cite as

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{becker_et_al:DARTS.8.2.10,
  author =	{Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
  title =	{{Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.10},
  URN =		{urn:nbn:de:0030-drops-162086},
  doi =		{10.4230/DARTS.8.2.10},
  annote =	{Keywords: compiler verification, compiler optimization, floating-point arithmetic}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.12
REST: Integrating Term Rewriting with Program Verification (Artifact)

Authors: Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
This artifact contains code for REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. The artifact includes the REST library as well as a version of Liquid Haskell extended with REST. In addition, it includes the scripts that were used to generate the tables in the paper’s evaluation section. Also included is a docker image containing a development environment for REST (and the Liquid Haskell extension).
Cite as

Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{grannan_et_al:DARTS.8.2.12,
  author =	{Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  title =	{{REST: Integrating Term Rewriting with Program Verification (Artifact)}},
  pages =	{12:1--12:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.12},
  URN =		{urn:nbn:de:0030-drops-162105},
  doi =		{10.4230/DARTS.8.2.12},
  annote =	{Keywords: term rewriting, program verification, theorem proving}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.1
Verified Compilation and Optimization of Floating-Point Programs in CakeML

Authors: Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the "fast-math-style" optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
Cite as

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 1:1-1:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ECOOP.2022.1,
  author =	{Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
  title =	{{Verified Compilation and Optimization of Floating-Point Programs in CakeML}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{1:1--1:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.1},
  URN =		{urn:nbn:de:0030-drops-162290},
  doi =		{10.4230/LIPIcs.ECOOP.2022.1},
  annote =	{Keywords: compiler verification, compiler optimization, floating-point arithmetic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.13
REST: Integrating Term Rewriting with Program Verification

Authors: Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell’s evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching (as used in most SMT solvers) and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs.
Cite as

Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 13:1-13:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{grannan_et_al:LIPIcs.ECOOP.2022.13,
  author =	{Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  title =	{{REST: Integrating Term Rewriting with Program Verification}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{13:1--13:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.13},
  URN =		{urn:nbn:de:0030-drops-162416},
  doi =		{10.4230/LIPIcs.ECOOP.2022.13},
  annote =	{Keywords: term rewriting, program verification, theorem proving}
}
Document
DOI: 10.4230/DagRep.11.6.147
Approximate Systems (Dagstuhl Seminar 21302)

Authors: Eva Darulova, Babak Falsafi, Andreas Gerstlauer, and Phillip Stanley-Marbell

Published in: Dagstuhl Reports, Volume 11, Issue 6 (2021)

Abstract
This report summarizes the presentations and discussion sessions at the Dagstuhl Seminar 21302 "Approximate Systems" that took place during July 25 - 30, 2021. Due to COVID, the seminar was held in a hybrid fashion, with around 1/3 of the attendees on-site and the remaining ones online. The seminar discussed advances and open challenges in applying approximate computing techniques across the stack and across different application domains, and we hope that this report can provide a useful resource also for other researchers.
Cite as

Eva Darulova, Babak Falsafi, Andreas Gerstlauer, and Phillip Stanley-Marbell. Approximate Systems (Dagstuhl Seminar 21302). In Dagstuhl Reports, Volume 11, Issue 6, pp. 147-163, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{darulova_et_al:DagRep.11.6.147,
  author =	{Darulova, Eva and Falsafi, Babak and Gerstlauer, Andreas and Stanley-Marbell, Phillip},
  title =	{{Approximate Systems (Dagstuhl Seminar 21302)}},
  pages =	{147--163},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2021},
  volume =	{11},
  number =	{6},
  editor =	{Darulova, Eva and Falsafi, Babak and Gerstlauer, Andreas and Stanley-Marbell, Phillip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.6.147},
  URN =		{urn:nbn:de:0030-drops-155836},
  doi =		{10.4230/DagRep.11.6.147},
  annote =	{Keywords: approximate computing, energy-efficient computing, pareto optimization}
}
Document
DOI: 10.4230/DagRep.7.8.74
Analysis and Synthesis of Floating-point Programs (Dagstuhl Seminar 17352)

Authors: Eva Darulova, Alastair F. Donaldson, Zvonimir Rakamaric, and Cindy Rubio-González

Published in: Dagstuhl Reports, Volume 7, Issue 8 (2018)

Abstract
This report summarises the presentations, discussion sessions and panel that took place during the Dagstuhl seminar on "Analysis and Synthesis of Floating-point Programs" that took place during August 27 - 30, 2017. We hope that the report will provide a useful resource for researchers today who are interested in understanding the state-of-the-art and open problems related to analysing and synthesising floating-point programs, and as a historical resource helping to clarify the status of this field in 2017.
Cite as

Eva Darulova, Alastair F. Donaldson, Zvonimir Rakamaric, and Cindy Rubio-González. Analysis and Synthesis of Floating-point Programs (Dagstuhl Seminar 17352). In Dagstuhl Reports, Volume 7, Issue 8, pp. 74-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{darulova_et_al:DagRep.7.8.74,
  author =	{Darulova, Eva and Donaldson, Alastair F. and Rakamaric, Zvonimir and Rubio-Gonz\'{a}lez, Cindy},
  title =	{{Analysis and Synthesis of Floating-point Programs (Dagstuhl Seminar 17352)}},
  pages =	{74--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{8},
  editor =	{Darulova, Eva and Donaldson, Alastair F. and Rakamaric, Zvonimir and Rubio-Gonz\'{a}lez, Cindy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.8.74},
  URN =		{urn:nbn:de:0030-drops-84318},
  doi =		{10.4230/DagRep.7.8.74},
  annote =	{Keywords: energy-efficient computing, floating-point arithmetic, precision allocation, program optimization, rigorous compilation}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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