Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDEva Darulova
Person information
- affiliation: Uppsala University, Sweden
- affiliation (former): Max Planck Institute for Software Systems
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2014
[b1]Eva Darulova:
Programming with Numerical Uncertainties. EPFL, Switzerland, 2014
Journal Articles
- 2023
- [j11]Rosa Abbasi
, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt:
Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY. Int. J. Softw. Tools Technol. Transf. 25(2): 185-204 (2023) - [j10]Debasmita Lohar, Clothilde Jeangoudoux, Anastasia Volkova, Eva Darulova:
Sound Mixed Fixed-Point Quantization of Neural Networks. ACM Trans. Embed. Comput. Syst. 22(5s): 136:1-136:26 (2023) - 2022
- [j9]Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox:
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). Dagstuhl Artifacts Ser. 8(2): 10:1-10:2 (2022) - [j8]Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers:
REST: Integrating Term Rewriting with Program Verification (Artifact). Dagstuhl Artifacts Ser. 8(2): 12:1-12:2 (2022) - [j7]Armin Alaghi, Eva Darulova, Andreas Gerstlauer, Phillip Stanley-Marbell:
Introduction to the Special Issue on Approximate Systems. ACM Trans. Design Autom. Electr. Syst. 27(2): 10:1-10:2 (2022) - 2021
- [j6]Phillip Stanley-Marbell, Armin Alaghi, Michael Carbin, Eva Darulova, Lara Dolecek, Andreas Gerstlauer, Ghayoor Gillani, Djordje Jevdjic, Thierry Moreau, Mattia Cacciotti, Alexandros Daglis, Natalie D. Enright Jerger, Babak Falsafi, Sasa Misailovic, Adrian Sampson, Damien Zufferey:
Exploiting Errors for Efficiency: A Survey from Circuits to Applications. ACM Comput. Surv. 53(3): 51:1-51:39 (2021) - [j5]Robert Rabe, Anastasiia Izycheva, Eva Darulova:
Regime Inference for Sound Floating-Point Optimizations. ACM Trans. Embed. Comput. Syst. 20(5s): 81:1-81:23 (2021) - 2020
- [j4]Ivan Gavran, Eva Darulova, Rupak Majumdar:
Interactive synthesis of temporal specifications from examples and natural language. Proc. ACM Program. Lang. 4(OOPSLA): 201:1-201:26 (2020) - 2019
- [j3]Mahmoud Salamati, Rocco Salvia, Eva Darulova, Sadegh Soudjani, Rupak Majumdar:
Memory-Efficient Mixed-Precision Implementations for Robust Explicit Model Predictive Control. ACM Trans. Embed. Comput. Syst. 18(5s): 100:1-100:19 (2019) - 2018
- [j2]Debasmita Lohar, Eva Darulova, Sylvie Putot, Eric Goubault:
Discrete Choice in the Presence of Numerical Uncertainties. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11): 2381-2392 (2018) - 2017
- [j1]Eva Darulova, Viktor Kuncak:
Towards a Compiler for Reals. ACM Trans. Program. Lang. Syst. 39(2): 8:1-8:28 (2017)
Conference and Workshop Papers
- 2023
- [c27]Rosa Abbasi, Eva Darulova:
Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs. SAS 2023: 41-64 - [c26]Anastasia Isychev, Eva Darulova:
Scaling up Roundoff Analysis of Functional Data Structure Programs. SAS 2023: 371-402 - 2022
- [c25]Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox:
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP 2022: 1:1-1:28 - [c24]Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers:
REST: Integrating Term Rewriting with Program Verification. ECOOP 2022: 13:1-13:29 - [c23]Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin:
Dandelion: Certified Approximations of Elementary Functions. ITP 2022: 6:1-6:19 - [c22]Jonas Krämer, Lionel Blatter, Eva Darulova, Mattias Ulbrich:
Inferring Interval-Valued Floating-Point Preconditions. TACAS (1) 2022: 303-321 - 2021
- [c21]Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar:
Lassie: HOL4 tactics by example. CPP 2021: 212-223 - [c20]Clothilde Jeangoudoux, Eva Darulova, Christoph Quirin Lauter:
Interval constraint-based mutation testing of numerical specifications. ISSTA 2021: 388-399 - [c19]Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis:
A Two-Phase Approach for Conditional Floating-Point Verification. TACAS (2) 2021: 43-63 - [c18]Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt:
Deductive Verification of Floating-Point Java Programs in KeY. TACAS (2) 2021: 242-261 - 2020
- [c17]Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock:
Synthesizing structured CAD models with equality saturation and inverse transformations. PLDI 2020: 31-44 - [c16]Anastasiia Izycheva, Eva Darulova, Helmut Seidl:
Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis. SAS 2020: 156-177 - [c15]Eva Darulova:
Towards a sound approximating compiler for numerical kernels (keynote). SCALA@SPLASH 2020: 1 - 2019
- [c14]Anastasiia Izycheva, Eva Darulova, Helmut Seidl:
Synthesizing Efficient Low-Precision Kernels. ATVA 2019: 294-313 - [c13]Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock:
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. CAV (2) 2019: 155-173 - [c12]Eva Darulova, Anastasia Volkova:
Sound Approximation of Programs with Elementary Functions. CAV (2) 2019: 174-183 - [c11]Joachim Bard, Heiko Becker, Eva Darulova:
Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions. FM 2019: 38-44 - [c10]Debasmita Lohar, Milos Prokop, Eva Darulova:
Sound Probabilistic Numerical Error Analysis. IFM 2019: 322-340 - 2018
- [c9]Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock:
Combining Tools for Optimization and Analysis of Floating-Point Computations. FM 2018: 355-363 - [c8]Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox:
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. FMCAD 2018: 1-10 - [c7]Eva Darulova, Einar Horn, Saksham Sharma:
Sound mixed-precision optimization with rewriting. ICCPS 2018: 208-219 - [c6]Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, Robert Bastian:
Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper). TACAS (1) 2018: 270-287 - 2017
- [c5]Anastasiia Izycheva, Eva Darulova:
On sound relative error bounds for floating-point arithmetic. FMCAD 2017: 15-22 - 2014
- [c4]Eva Darulova, Viktor Kuncak:
Sound compilation of reals. POPL 2014: 235-248 - 2013
- [c3]Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha:
Synthesis of fixed-point programs. EMSOFT 2013: 22:1-22:10 - 2012
- [c2]Eva Darulova, Viktor Kuncak:
Certifying Solutions for Numerical Constraints. RV 2012: 277-291 - 2011
- [c1]Eva Darulova, Viktor Kuncak:
Trustworthy numerical computation in Scala. OOPSLA 2011: 325-344
Informal and Other Publications
- 2022
- [i16]Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin:
Dandelion: Certified Approximations of Elementary Functions. CoRR abs/2202.05472 (2022) - [i15]Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers:
REST: Integrating Term Rewriting with Program Verification (Extended Version). CoRR abs/2202.05872 (2022) - 2021
- [i14]Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar:
Lassie: HOL4 Tactics by Example. CoRR abs/2101.00930 (2021) - [i13]Rosa Abbasi Boroujeni, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt:
Deductive Verification of Floating-Point Java Programs in KeY. CoRR abs/2101.08733 (2021) - [i12]Eva Darulova, Babak Falsafi, Andreas Gerstlauer, Phillip Stanley-Marbell:
Approximate Systems (Dagstuhl Seminar 21302). Dagstuhl Reports 11(6): 147-163 (2021) - 2019
- [i11]Chandrakana Nandi, Adam Anderson, Max Willsey, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock:
Using E-Graphs for CAD Parameter Inference. CoRR abs/1909.12252 (2019) - 2018
- [i10]Brendon Boldt, Ivan Gavran, Eva Darulova, Rupak Majumdar:
Precise but Natural Specification for Robot Tasks. CoRR abs/1803.02238 (2018) - [i9]Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock:
Combining Tools for Optimization and Analysis of Floating-Point Computations. CoRR abs/1805.02436 (2018) - [i8]Phillip Stanley-Marbell, Armin Alaghi, Michael Carbin, Eva Darulova, Lara Dolecek, Andreas Gerstlauer, Ghayoor Gillani, Djordje Jevdjic, Thierry Moreau, Mattia Cacciotti, Alexandros Daglis, Natalie D. Enright Jerger, Babak Falsafi, Sasa Misailovic, Adrian Sampson, Damien Zufferey:
Exploiting Errors for Efficiency: A Survey from Circuits to Algorithms. CoRR abs/1809.05859 (2018) - [i7]Eva Darulova, Anastasia Volkova:
Sound Approximation of Programs with Elementary Functions. CoRR abs/1811.10274 (2018) - 2017
- [i6]Heiko Becker, Eva Darulova, Magnus O. Myreen:
A Verified Certificate Checker for Floating-Point Error Bounds. CoRR abs/1707.02115 (2017) - [i5]Eva Darulova, Einar Horn, Saksham Sharma:
Sound Mixed-Precision Optimization with Rewriting. CoRR abs/1707.02118 (2017) - [i4]Anastasiia Izycheva, Eva Darulova:
On Sound Relative Error Bounds for Floating-Point Arithmetic. CoRR abs/1707.02121 (2017) - [i3]Eva Darulova, Alastair F. Donaldson, Zvonimir Rakamaric, Cindy Rubio-González:
Analysis and Synthesis of Floating-point Programs (Dagstuhl Seminar 17352). Dagstuhl Reports 7(8): 74-101 (2017) - 2014
- [i2]Eva Darulova, Viktor Kuncak:
On Numerical Error Propagation with Sensitivity. CoRR abs/1410.0198 (2014) - 2013
- [i1]Eva Darulova, Viktor Kuncak:
On Sound Compilation of Reals. CoRR abs/1309.2511 (2013)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-09 00:02 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
