Automatisierte Verifikation und Synthese von Approximationen

• Antragstellerin: Eva Darulova, Ph.D.
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2017 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 387674182

Computerressourcen sind grundsätzlich begrenzt und manchmal existiert eine genaue Lösung nicht einmal. Daher sind bei der Implementierung von realen Systemen Approximationen unvermeidlich - ebenso wie die Fehler, die sie produzieren. Das Ausmass der Fehler ist problemabhängig, aber generell kostet eine höhere Genauigkeit in Bezug auf Speicherplatz, Energie oder Laufzeit immer mehr und kreiert so einen Präzisions-Effizienz-Kompromiss. Um die Vorteile dieses Kompromisses nutzen zu können, müssen wir sicherstellen, dass die berechneten Ergebnisse hinreichend genau sind, sonst riskieren wir katastrophal falsche Ergebnisse oder sogar Systemausfälle. Leider ist die aktuelle Art der Programmierung mit Approximationen meist manuell, und folglich teuer, fehleranfällig und führt häufig zu suboptimalen Ergebnissen.Das Ziel dieses Projektes ist es ein End-to-End System zu entwickeln, welches numerische Programme automatisch und vertrauenswürdig approximiert. Der Programmierer wird dann in der Lage sein, präzisen high-level Code zu schreiben und unser 'approximierender Compiler' wird automatisch eine effiziente Implementierung generieren, die eine vorgegebene Genauigkeit erfüllt. Um diese Vision zu erreichen, werden wir neuartige Methoden entwickeln, die die Präzision von numerischen Programmen verifizieren, sowie neue Syntheseansätze erforschen, die solche Approximationen automatisch generieren.

• DFG-Verfahren: Sachbeihilfen