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

• Heiko Becker
• Debasmita Lohar
• Rosa Abbasi
• Anastasiia Izycheva (co-advisor)

Postdocs

• Clothilde Jeangoudoux

Teaching

• Program Design and Data Structures (2021/22)
• 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: ASPLOS'22 artifact evaluation chair, ECOOP'22, ESEC/FSE'22
• recent: EMSOFT'21 (PC), PLDI'21 (PC)

Publications

• 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
  

Alumni

• Mustafa Hafidi (MSc'20)
• Joachim Bard (MSc'19)
• Nikita Zyuzin (MSc'19)
• Youcef Merah (MSc'18)
• Safya Alzayat (BSc'18)
• Anastasiia Izycheva (MSc'17)

Snail Mail

Box 337
751 05 Uppsala

Visiting Address

room 1320
Lägerhyddsvägen 2, house 1
752 37 Uppsala

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