Synthesis with Uncertainties
Eva Darulova
Max Planck Institute for Software Systems (MPI-SWS)
Abstract:
In this talk, I will present three of my recent synthesis projects that, while having quite different goals and also equally varied solutions, have in common that uncertainties are a major challenge in finding reliable solutions. In particular, I will show how to:
- automatically approximate a numerical kernel with elementary function calls while guaranteeing an end-to-end bound on the approximation error;
- obtain tight loop invariants for floating-point loops, leveraging their ‘noisy’ nature due to roundoff errors;
- synthesize LTL robot specifications from (ambiguous) natural language commands and a single example, using two complementary techniques for generalization.