Formal Verification of Industrial Software and Neural Networks

Software ist ein wichtiger Bestandteil unsere heutige Gesellschaft. Da Software vermehrt
in sicherheitskritischen Bereichen angewandt wird, müssen wir uns auf eine korrekte und
sichere Ausführung verlassen können. Besonders eingebettete Software, zum Beispiel in
medizinischen Geräten, Autos oder Flugzeugen, muss gründlich und formal geprüft werden.
Die Software solcher eingebetteten Systeme kann man in zwei Komponenten aufgeteilt.
In klassische (deterministische) Steuerungssoftware und maschinelle Lernverfahren
zum Beispiel für die Bilderkennung oder Kollisionsvermeidung angewandt werden.
... mehr
Das Ziel dieser Dissertation ist es den Stand der Technik bei der Verifikation von
zwei Hauptkomponenten moderner eingebetteter Systeme zu verbessern: in C/C++
geschriebene Software und neuronalen Netze. Für beide Komponenten wird das Verifikationsproblem
formal definiert und neue Verifikationsansätze werden vorgestellt.

Software has become an integral part of today’s society. As software is increasingly
applied in safety-critical areas, we must be able to rely on its correct and safe execution.
Especially embedded software, for example in medical devices, cars or airplanes, must
be thoroughly and formally verified. The software of such embedded systems can be
divided into two kind of components. Traditionally engineered control software and
machine learning methods as applied for image recognition or collision avoidance.
This dissertations aims to improve the state-of-the-art for the verification of two main
... mehr
components of modern embedded systems: software written in C/C++ and neural networks.
Verification for both components is formally defined and novel verification approaches
are presented.