Eva Darulova

Projects

• Blossom - a guided blackbox fuzzer to infer numerical kernel ranges
• Lassie - HOL4 tactics by example
• Pine - synthesizer for floating-point numerical loops
• LTLTalk - instructing robots by example
• Incarnate - PL Tools and Techniques for 3D Printing
• Icing - a nondeterministic floating-point source semantics
• Flipper - a natural language robot interface
• FloVer - a certificate checker for roundoff error bounds
• Daisy - a framework for accuracy analysis and synthesis of numerical programs
• Rosa - the real compiler

PhD Students

• Debasmita Lohar
• Rosa Abbasi
• Amanda Stjerna

Alumni

• Anastasia Isychev (co-advised PhD 2023)
• Heiko Becker (PhD 2022)
• Clothilde Jeangoudoux (postdoc June’19–Dec’21)

Teaching

• Program Design and Data Structures (2021/22, 22/23, 23/24)
• PhD course on Introduction to Programming Language Research (2022, 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)

Service

• current/upcoming: ICSE'24, ECOOP'24
• recent: ECOOP'22, ESEC/FSE'22, ASPLOS'22 artifact evaluation chair

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
  

Snail Mail

Box 337
751 05 Uppsala

Visiting Address

room 105141
Lägerhyddsvägen 1, house 10
752 37 Uppsala

* I continue to use my birth name on scientific publications.