Max Planck Institute for Software Systems (MPI-SWS)
Paul-Ehrlich-Strasse, Building G 26
room 417, Kaiserslautern
eva at mpi - sws dot org
+49 681 9303-8101
I am a tenure-track faculty at MPI-SWS. Before that, I did my PhD
with Viktor Kuncak at EPFL.
I am generally interested in programming languages, software verification, program synthesis and approximate computing.
Currently, my focus lies on applications in numerical, embedded or cyber-physical domains.
Internship and MSc projects: in case you are interested
drop me an email with a brief statement of interest and your CV.
- current: Correctness'20, PLDI'21
- recent: CAV'20 (PC), PLDI'20 (ERC), VSTTE'20 (PC), ECOOP'19 (PC), CAV'19 (PC), OOPSLA'19 (ERC), WAX'19 (PC), FHPNC'19 (PC), PLDI'18 (PC, SRC), CAV'18 (AEC), iFM (PC), CGO'18 (PC)
Interactive Synthesis of Temporal Specifications from Examples and Natural Language
conditionally accepted at OOPSLA'20
Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis
Exploiting Errors for Efficiency: A Survey from Circuits to Algorithms,
ACM Computing Surveys, June 2020
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations,
Sound Probabilistic Numerical Error Analysis,
Memory-Efficient Mixed-Precision Implementations for Robust Explicit Model Predictive Control,
Synthesizing Efficient Low-Precision Kernels,
Formally Verified Roundoff Errors using SMT-based Certificates and Subdivisions,
Icing: Supporting Fast-math Style Optimizations in a Verified Compiler,
Sound Approximation of Programs with Elementary Functions,
Precise but Natural Specification for Robot Tasks
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Discrete Choice in the Presence of Numerical Uncertainties
Combining Tools for Optimization and Analysis of Floating-Point Computations
Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper)
Sound Mixed-Precision Optimization with Rewriting
On Sound Relative Error Bounds for Floating-Point Arithmetic
Towards a Compiler for Reals
E. Darulova, V. Kuncak, ACM Transactions on Programming Languages and Systems (TOPLAS), 2017
Programming with Numerical Uncertainties
EPFL PhD thesis 2014
- Sound Compilation of Reals.
- Programming Language and Compiler Support for Uncertainties
First SIGPLAN Workshop on Probabilistic and Approximate Computing (APPROX'14).
Co-located with PLDI 2014 in Edinburgh, Scotland. Invited Position Paper
- Synthesis of Fixed-Point Programs
- Certifying Solutions for Numerical Constraints
- Trustworthy Numerical Computation in Scala
- Joachim Bard (MSc'19)
- Nikita Zyuzin (MSc'19)
- Youcef Merah (MSc'18)
- Safya Alzayat (BSc'18)
- Anastasiia Izycheva (MSc'17)
Paul-Ehrlich-Strasse, G 26