Eva Darulova

58 papers A* 2A 4B 12Misc 1Journal 29Unranked 9
YearRankTypeTitle / Venue / Authors
2026 — conf
Verifying Floating-Point Programs in Stainless.
TACAS (2)
Andrea Gilot, Axel Bergström, Eva Darulova
2026 J jnl
Verifying Floating-Point Programs in Stainless.
CoRR
Andrea Gilot, Axel Bergström, Eva Darulova
2025 J jnl
A Large-Scale Study of Floating-Point Usage in Statically Typed Languages.
CoRR
Andrea Gilot, Tobias Wrigstad, Eva Darulova
2023 J jnl
Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY.
Int. J. Softw. Tools Technol. Transf.
Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt
2023 B conf
Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs.
SAS
Rosa Abbasi, Eva Darulova
2023 B conf
Scaling up Roundoff Analysis of Functional Data Structure Programs.
SAS
Anastasia Isychev, Eva Darulova
2023 J jnl
Sound Mixed Fixed-Point Quantization of Neural Networks.
ACM Trans. Embed. Comput. Syst.
Debasmita Lohar, Clothilde Jeangoudoux, Anastasia Volkova, Eva Darulova
2022 B conf
Dandelion: Certified Approximations of Elementary Functions.
ITP
Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin
2022 J jnl
Dandelion: Certified Approximations of Elementary Functions.
CoRR
Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin
2022 — conf
Inferring Interval-Valued Floating-Point Preconditions.
TACAS (1)
Jonas Krämer, Lionel Blatter, Eva Darulova, Mattias Ulbrich
2022 J jnl
Introduction to the Special Issue on Approximate Systems.
ACM Trans. Design Autom. Electr. Syst.
Armin Alaghi, Eva Darulova, Andreas Gerstlauer, Phillip Stanley-Marbell
2022 J jnl
REST: Integrating Term Rewriting with Program Verification (Artifact).
Dagstuhl Artifacts Ser.
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
2022 J jnl
REST: Integrating Term Rewriting with Program Verification (Extended Version).
CoRR
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
2022 A conf
REST: Integrating Term Rewriting with Program Verification.
ECOOP
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
2022 J jnl
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact).
Dagstuhl Artifacts Ser.
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
2022 A conf
Verified Compilation and Optimization of Floating-Point Programs in CakeML.
ECOOP
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
2021 — conf
A Two-Phase Approach for Conditional Floating-Point Verification.
TACAS (2)
Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis
2021 J jnl
Approximate Systems (Dagstuhl Seminar 21302).
Dagstuhl Reports
Eva Darulova, Babak Falsafi, Andreas Gerstlauer, Phillip Stanley-Marbell
2021 — conf
Deductive Verification of Floating-Point Java Programs in KeY.
TACAS (2)
Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt
2021 J jnl
Deductive Verification of Floating-Point Java Programs in KeY.
CoRR
Rosa Abbasi Boroujeni, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt
2021 J jnl
Exploiting Errors for Efficiency: A Survey from Circuits to Applications.
ACM Comput. Surv.
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
2021 A conf
Interval constraint-based mutation testing of numerical specifications.
ISSTA
Clothilde Jeangoudoux, Eva Darulova, Christoph Quirin Lauter
2021 J jnl
Lassie: HOL4 Tactics by Example.
CoRR
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar
2021 B conf
Lassie: HOL4 tactics by example.
CPP
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar
2021 J jnl
Regime Inference for Sound Floating-Point Optimizations.
ACM Trans. Embed. Comput. Syst.
Robert Rabe, Anastasiia Izycheva, Eva Darulova
2020 B conf
Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis.
SAS
Anastasiia Izycheva, Eva Darulova, Helmut Seidl
2020 J jnl
Interactive synthesis of temporal specifications from examples and natural language.
Proc. ACM Program. Lang.
Ivan Gavran, Eva Darulova, Rupak Majumdar
2020 A* conf
Synthesizing structured CAD models with equality saturation and inverse transformations.
PLDI
Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock
2020 — conf
Towards a sound approximating compiler for numerical kernels (keynote).
SCALA@SPLASH
Eva Darulova
2019 B conf
Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions.
FM
Joachim Bard, Heiko Becker, Eva Darulova
2019 — conf
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler.
CAV (2)
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
2019 J jnl
Memory-Efficient Mixed-Precision Implementations for Robust Explicit Model Predictive Control.
ACM Trans. Embed. Comput. Syst.
Mahmoud Salamati, Rocco Salvia, Eva Darulova, Sadegh Soudjani, Rupak Majumdar
2019 — conf
Sound Approximation of Programs with Elementary Functions.
CAV (2)
Eva Darulova, Anastasia Volkova
2019 B conf
Sound Probabilistic Numerical Error Analysis.
IFM
Debasmita Lohar, Milos Prokop, Eva Darulova
2019 B conf
Synthesizing Efficient Low-Precision Kernels.
ATVA
Anastasiia Izycheva, Eva Darulova, Helmut Seidl
2019 J jnl
Using E-Graphs for CAD Parameter Inference.
CoRR
Chandrakana Nandi, Adam Anderson, Max Willsey, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock
2018 B conf
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.
FMCAD
Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox
2018 B conf
Combining Tools for Optimization and Analysis of Floating-Point Computations.
FM
Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock
2018 J jnl
Combining Tools for Optimization and Analysis of Floating-Point Computations.
CoRR
Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock
2018 — conf
Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper).
TACAS (1)
Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, Robert Bastian
2018 J jnl
Discrete Choice in the Presence of Numerical Uncertainties.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Debasmita Lohar, Eva Darulova, Sylvie Putot, Eric Goubault
2018 J jnl
Exploiting Errors for Efficiency: A Survey from Circuits to Algorithms.
CoRR
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
2018 J jnl
Precise but Natural Specification for Robot Tasks.
CoRR
Brendon Boldt, Ivan Gavran, Eva Darulova, Rupak Majumdar
2018 J jnl
Sound Approximation of Programs with Elementary Functions.
CoRR
Eva Darulova, Anastasia Volkova
2018 — conf
Sound mixed-precision optimization with rewriting.
ICCPS
Eva Darulova, Einar Horn, Saksham Sharma
2017 J jnl
A Verified Certificate Checker for Floating-Point Error Bounds.
CoRR
Heiko Becker, Eva Darulova, Magnus O. Myreen
2017 J jnl
Analysis and Synthesis of Floating-point Programs (Dagstuhl Seminar 17352).
Dagstuhl Reports
Eva Darulova, Alastair F. Donaldson, Zvonimir Rakamaric, Cindy Rubio-González
2017 J jnl
On Sound Relative Error Bounds for Floating-Point Arithmetic.
CoRR
Anastasiia Izycheva, Eva Darulova
2017 B conf
On sound relative error bounds for floating-point arithmetic.
FMCAD
Anastasiia Izycheva, Eva Darulova
2017 J jnl
Sound Mixed-Precision Optimization with Rewriting.
CoRR
Eva Darulova, Einar Horn, Saksham Sharma
2017 J jnl
Towards a Compiler for Reals.
ACM Trans. Program. Lang. Syst.
Eva Darulova, Viktor Kuncak
2014 J jnl
On Numerical Error Propagation with Sensitivity.
CoRR
Eva Darulova, Viktor Kuncak
2014 — —
Programming with Numerical Uncertainties.
Eva Darulova
2014 A* conf
Sound compilation of reals.
POPL
Eva Darulova, Viktor Kuncak
2013 J jnl
On Sound Compilation of Reals.
CoRR
Eva Darulova, Viktor Kuncak
2013 Misc conf
Synthesis of fixed-point programs.
EMSOFT
Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha
2012 B conf
Certifying Solutions for Numerical Constraints.
RV
Eva Darulova, Viktor Kuncak
2011 A conf
Trustworthy numerical computation in Scala.
OOPSLA
Eva Darulova, Viktor Kuncak