Eva Darulova

Projects

Active projects:

• HORNET
  automated techniques for verifying and debugging real-world numerical programs
• A Large-Scale Code Study of Floating-Point Usage
  Preprint: [Arxiv]
• Daisy - a framework for accuracy analysis and synthesis of numerical programs
  integrates several different sound static analyses and optimizations for floating-point and fixed-point programs, covering absolute and relative rounding errors for arithmetic [TACAS'18] [FMCAD'17], array-like data structures [SAS'23] and function calls [SAS'23], mixed-precision tuning and rewriting optimizations [ICCPS'18] [EMSOFT'21], probabilistic analyses [EMSOFT'18] [iFM'19], approximations of elementary functions [CAV'19] [ATVA'19], and specification inference [TACAS'22].
  source code

Previous projects:

• Aster - a sound mixed fixed-point quantizer for neural networks [EMSOFT'23] | source code
• Blossom - a guided blackbox fuzzer to infer numerical kernel ranges [TACAS'21] | source code
• Lassie - HOL4 tactics by example [CPP'21] | source code
• Pine - synthesizer for floating-point numerical loops [SAS'20] | source code
• LTLTalk - instructing robots by example [OOPSLA'20] | project page
• Incarnate - PL Tools and Techniques for 3D Printing [PLDI'20] | project page
• Icing - a nondeterministic floating-point source semantics [CAV'19] [ECOOP'22] | source code
• Flipper - a natural language robot interface project page
• FloVer - a certificate checker for roundoff error bounds [FMCAD'18] [FM'19] | source code
• Rosa - the real compiler [POPL'14] [TOPLAS'17] | source code

PhD Students

• Axel Bergström
• Andrea Gilot
• Amanda Stjerna
• Rosa Abbasi

Publications

• Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs. Rosa Abbasi, Eva Darulova.
  SAS'23 | paper | code
• Scaling up Roundoff Analysis of Functional Data Structure Programs. Anastasia Isychev, Eva Darulova.
  SAS'23 | paper
• Sound Mixed Fixed-Point Quantization of Neural Networks. Debasmita Lohar, Clothilde Jeangoudoux, Anastasia Volkova and Eva Darulova.
  EMSOFT'23 | paper | code
• Combining Rule- and SMT-Based Reasoning for Verifying Floating-Point Java Programs in KeY. Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich and Wolfgang Ahrendt.
  International Journal on Software Tools for Technology Transfer (STTT), 2023, TACAS'21 special issue | paper
  
• Dandelion: Certified Approximations of Elementary Functions. Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova and Jean-Baptiste Jeannin.
  ITP'22 | paper | code
• Verified Compilation and Optimization of Floating-Point Programs in CakeML. Heiko Becker, Robert Rabe, Eva Darulova, Magnus Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony Fox.
  ECOOP'22 | paper
• REST: Integrating Term Rewriting with Program Verification. Zachary Grannan, Eva Darulova, Alexander J. Summers, Niki Vazou.
  ECOOP'22 | paper
• Inferring Interval-Valued Floating-Point Preconditions. Jonas Krämer, Lionel Blatter, Eva Darulova and Mattias Ulbrich.
  TACAS'22 | paper | code
• Regime Inference for Sound Floating-Point Optimizations. Robert Rabe, Anastasiia Izycheva, Eva Darulova.
  EMSOFT'21 | paper | code
• A Roadmap Towards Parallel Printing for Desktop 3D Printers. Molly Aubrey Carton, Chandrakana Nandi, Adam Anderson, Haisen Zhao, Eva Darulova, Dan Grossman, Jeffrey I. Lipton, Adriana Schulz, Zachary Tatlock.
  Solid Freeform Fabrication Symposium (SFF) 2021 | paper
• Interval Constraint-Based Mutation Testing of Numerical Specifications. Clothilde Jeangoudoux, Eva Darulova and Christoph Lauter.
  ISSTA'21 | paper | code | Clothilde's talk video
• A Two-Phase Approach for Conditional Floating-Point Verification. Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova and Maria Christakis.
  TACAS'21 | paper | code | Debasmita's talk video
• Deductive Verification of Floating-Point Java Programs in KeY. Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich and Wolfgang Ahrendt.
  TACAS'21 | paper | nominated for the EAPLS best paper award
• Lassie: HOL4 Tactics by Example. Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova and Rupak Majumdar.
  CPP'21 | paper | code | Heiko's talk video
  
• Interactive Synthesis of Temporal Specifications from Examples and Natural Language Ivan Gavran, Eva Darulova and Rupak Majumdar.
  OOPSLA'20 | paper | code | try online | Ivan's talk video
  
• Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis Anastasiia Izycheva, Eva Darulova and Helmut Seidl.
  SAS'20 | paper | code | Anastasiia's talk video
  
• Exploiting Errors for Efficiency: A Survey from Circuits to Algorithms, Phillip Stanley-Marbell, Armin Alaghi, Michael Carbin, Eva Darulova, Lara Dolecek, Andreas Gerstlauer, Ghayoor Gillani, Djordje Jevdjic, Thierry Moreau, Mattia Cacciotti, Alexandros Daglis, Natalie Enright Jerger, Babak Falsafi, Sasa Misailovic, Adrian Sampson and Damien Zufferey.
  ACM Computing Surveys, June 2020 | paper
  
• Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations, Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman and Zachary Tatlock.
  PLDI'20 | paper | code | Chandra's talk video
  
• Sound Probabilistic Numerical Error Analysis, Debasmita Lohar, Milos Prokop and Eva Darulova.
  iFM'19 | paper | code
• Memory-Efficient Mixed-Precision Implementations for Robust Explicit Model Predictive Control, Mahmoud Salamati, Rocco Salvia, Eva Darulova, Sadegh Soudjani and Rupak Majumdar.
  EMSOFT'19 | paper
  
• Synthesizing Efficient Low-Precision Kernels, Anastasiia Izycheva, Eva Darulova, and Helmut Seidl.
  ATVA'19 | paper | code
• Formally Verified Roundoff Errors using SMT-based Certificates and Subdivisions, Heiko Becker, Joachim Bard and Eva Darulova.
  FM'19 | paper | code
• Icing: Supporting Fast-math Style Optimizations in a Verified Compiler, Heiko Becker, Eva Darulova, Magnus O. Myreen and Zachary Tatlock.
  CAV'19 | paper | code
• Sound Approximation of Programs with Elementary Functions, Eva Darulova and Anastasia Volkova.
  CAV'19 | paper | code
• Precise but Natural Specification for Robot Tasks Ivan Gavran, Brendon Boldt, Eva Darulova and Rupak Majumdar.
  CoRR abs/1803.02238 | paper
  
• A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen and Anthony Fox.
  FMCAD'18 | paper | code
• Discrete Choice in the Presence of Numerical Uncertainties Debasmita Lohar, Eva Darulova, Sylvie Putot and Eric Goubault.
  EMSOFT'18 | paper | code
• Combining Tools for Optimization and Analysis of Floating-Point Computations Heiko Becker, Pavel Panchekha, Eva Darulova and Zachary Tatlock.
  FM'18 | paper
  
• Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper) Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker and Robert Bastian.
  TACAS'18 | paper | code
• Sound Mixed-Precision Optimization with Rewriting Eva Darulova, Einar Horn and Saksham Sharma.
  ICCPS'18 | paper | code
• On Sound Relative Error Bounds for Floating-Point Arithmetic Anastasiia Izycheva and Eva Darulova.
  FMCAD 2017 | paper | code
• Towards a Compiler for Reals Eva Darulova and Viktor Kuncak.
  ACM Transactions on Programming Languages and Systems (TOPLAS), 2017 | paper | code
• Programming with Numerical Uncertainties Eva Darulova, EPFL PhD thesis 2014 | pdf
  
• Sound Compilation of Reals Eva Darulova and Viktor Kuncak.
  POPL'14 | paper | code
• Synthesis of Fixed-Point Programs Eva Darulova, Viktor Kuncak, Indranil Saha and Rupak Majumdar.,
  EMSOFT'13 | paper
• Certifying Solutions for Numerical Constraints Eva Darulova and Viktor Kuncak.
  RV'12 | paper
  
• Trustworthy Numerical Computation in Scala Eva Darulova and Viktor Kuncak.
  OOPSLA'11 | paper
  

Recent Talks

• Recent Advances in Floating-point (Static) Analyses (Keynote at SOAP 2024) | video
• Recent Advances in Floating-point Static Analyses (Invited talk at KeY Symposium 2023)
• Taming Floating-Points in Scala and CakeML (Invited talk at Lambda Days 2022) | video
• Becoming a professor without planning to be one (Invited talk at ETAPS Mentoring workshop 2022)

Service

Teaching

• Program Design and Data Structures (2021/22, 22/23, 23/24, 24/25)
• PhD course on Introduction to Programming Language Research (2022, 2025, co-teaching with Elias Castegren and Tobias Wrigstad)
• Program Synthesis (seminar, summer 2021)
• Program Analysis (winter 20/21, winter 19/20, winter 18/19)
• Advanced Program Analysis (seminar, March 19)
• Program Synthesis (seminar, summer 2018)
• Static Program Analysis (summer 2017)
• Approximate Computing: Promise or Hype? (seminar, summer 2016)