| 2026 | TACAS | Verifying Floating-Point Programs in Stainless. | Andrea Gilot, Axel Bergstrm, Eva Darulova |
| 2023 | SAS | Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs. | Rosa Abbasi, Eva Darulova |
| 2023 | SAS | Scaling up Roundoff Analysis of Functional Data Structure Programs. | Anastasia Isychev, Eva Darulova |
| 2022 | ECOOP | Verified Compilation and Optimization of Floating-Point Programs in CakeML. | Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox |
| 2022 | ECOOP | REST: Integrating Term Rewriting with Program Verification. | Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers |
| 2022 | ITP | Dandelion: Certified Approximations of Elementary Functions. | Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin |
| 2022 | TACAS | Inferring Interval-Valued Floating-Point Preconditions. | Jonas Krmer, Lionel Blatter, Eva Darulova, Mattias Ulbrich |
| 2021 | CPP | Lassie: HOL4 tactics by example. | Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar |
| 2021 | ISSTA | Interval constraint-based mutation testing of numerical specifications. | Clothilde Jeangoudoux, Eva Darulova, Christoph Quirin Lauter |
| 2021 | TACAS | Deductive Verification of Floating-Point Java Programs in KeY. | Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt |
| 2021 | TACAS | A Two-Phase Approach for Conditional Floating-Point Verification. | Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis |
| 2020 | PLDI | Synthesizing structured CAD models with equality saturation and inverse transformations. | Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock |
| 2020 | SAS | Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis. | Anastasiia Izycheva, Eva Darulova, Helmut Seidl |
| 2019 | ATVA | Synthesizing Efficient Low-Precision Kernels. | Anastasiia Izycheva, Eva Darulova, Helmut Seidl |
| 2019 | CAV | Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. | Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock |
| 2019 | CAV | Sound Approximation of Programs with Elementary Functions. | Eva Darulova, Anastasia Volkova |
| 2019 | FM | Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions. | Joachim Bard, Heiko Becker, Eva Darulova |
| 2019 | IFM | Sound Probabilistic Numerical Error Analysis. | Debasmita Lohar, Milos Prokop, Eva Darulova |
| 2018 | FM | Combining Tools for Optimization and Analysis of Floating-Point Computations. | Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock |
| 2018 | FMCAD | A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. | Heiko Becker, Nikita Zyuzin, Raphal Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox |
| 2018 | TACAS | Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper). | Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, Robert Bastian |
| 2017 | FMCAD | On sound relative error bounds for floating-point arithmetic. | Anastasiia Izycheva, Eva Darulova |
| 2014 | POPL | Sound compilation of reals. | Eva Darulova, Viktor Kuncak |
| 2013 | EMSOFT | Synthesis of fixed-point programs. | Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha |
| 2012 | RV | Certifying Solutions for Numerical Constraints. | Eva Darulova, Viktor Kuncak |
| 2011 | OOPSLA | Trustworthy numerical computation in Scala. | Eva Darulova, Viktor Kuncak |