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

Postdocs

• Clothilde Jeangoudoux

Teaching

• Program Synthesis (summer 2021)
• Program Analysis (winter 20/21)
• Program Analysis (winter 19/20)
• Advanced Program Analysis (blockseminar march 19)
• Program Analysis (winter 18/19)
• Program Synthesis (summer 2018)
• Static Program Analysis (summer 2017)
• Approximate Computing: Promise or Hype? (summer 2016)

Service

• current: PLDI'21 (PC), EMSOFT'21 (PC)
• recent: Correctness'20 (PC), CAV'20 (PC), PLDI'20 (ERC), VSTTE'20 (PC), ECOOP'19 (PC), CAV'19 (PC), OOPSLA'19 (ERC), WAX'19 (PC), FHPNC'19 (PC)

Publications

• A Two-Phase Approach for Conditional Floating-Point Verification. Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova and Maria Christakis.
  TACAS'21 | paper | code
• Deductive Verification of Floating-Point Java Programs in KeY. Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich and Wolfgang Ahrendt.
  TACAS'21 | paper
• Lassie: HOL4 Tactics by Example. Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova and Rupak Majumdar.
  CPP'21 | paper | code
  
• 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

MPI-SWS
Paul-Ehrlich-Strasse, G 26
D-67663 Kaiserslautern
Germany