Automatisierte Verifikation und Synthese von Approximationen
Zusammenfassung der Projektergebnisse
Ziel des Projektes war die Entwicklung von Programmiertechniken zur automatisierten und fundierten Approximation numerischer Programme. Während numerische Annäherungen ein fester Bestandteil vieler eingebetteter und wissenschaftlicher Computersysteme sind, erfolgt ihre Programmierung heute weitgehend manuell. Das heißt, ein Entwickler muss auswählen, welche Annäherungen anzuwenden sind, und verifizieren, dass die resultierende Genauigkeit für die spezielle Anwendung ausreichend bleibt. Ohne automatisierte Verifizierungs- und Syntheseunterstützung ist dieser Prozess langwierig, fehleranfällig und führt häufig zu einer ineffizienten Nutzung verfügbarer Ressourcen. In diesem Projekt haben wir die Verifikationsfunktionalität des bestehenden Daisy-Frameworks zur Analyse numerischer Programme erweitert, um probabilistische Fehlerspezifikationen zu unterstützen. Solche Spezifikationen sind entscheidend, um eine weitere wichtige Klasse von Approximationen aufgrund von ungenauer Hardware zu unterstützen, die mit einer bestimmten Wahrscheinlichkeit einen größeren Fehler als erwartet erzeugen kann. Als nächstes haben wir uns mit der Skalierbarkeit der bestehenden automatisierten Verifikationstechniken befasst, indem wir eine Kombination aus statischen und dynamischen Analysen vorgeschlagen haben, die es ermöglicht, die soliden statischen Analysetechniken auf numerisch wichtige Teile eines größeren Programms anzuwenden. Hier sind wir etwas vom ursprünglichen Projektplan abgewichen, da die dynamische Analyse nicht innerhalb des Daisy-Frameworks implementiert ist. Wir haben uns dazu aus praktischen Gründen entschieden, um mit bestehenden Programmen, die in C/C++ geschrieben sind, umgehen zu können. Das Projekt hat aber eine Schnittstelle zu Daisy. Derzeit arbeiten wir an der Low-Level-Codegenerierung und Optimierung von Controllern für neuronale Netzwerke, die auf Field-Programmable Gate-Arrays (FPGAs) abzielen.
Projektbezogene Publikationen (Auswahl)
- Sound Probabilistic Numerical Error Analysis, iFM’19
Debasmita Lohar, Milos Prokop and Eva Darulova
(Siehe online unter https://doi.org/10.1007/978-3-030-34968-4_18) - A Two-Phase Approach for Conditional Floating-Point Verification. TACAS’21
Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova and Maria Christakis
(Siehe online unter https://doi.org/10.1007/978-3-030-72013-1_3)
