Samstag, 20.10.2018

Forschung

Preis des Fakultätentags Informatik für Anton Pirogov

Seine Masterarbeit im Studiengang Informatik der Universität zu Lübeck wurde als beste Abschlussarbeit 2018 ausgezeichnet

Anton Pirogov, Masterabsolvent des Studiengangs Informatik der Universität zu Lübeck, ist für seine Masterarbeit mit dem Preis des Fakultätentags Informatik für die beste Abschlussarbeit 2018 ausgezeichnet worden.

In seiner Arbeit „SMT-basiertes Flaches Model-Checking für LTL mit Zählquantoren“ untersucht Anton Pirogov die Frage, ob sich theoretische Ergebnisse der Pfadschemata in flachen Strukturen für die Verifikation von Softwaresystemen einsetzen lassen. Auf der theoretischen Seite entwickelt er dabei eine effiziente Kodierung in quantorenfreie Presburger Arithmetik, auf der praktischen Seite implementiert und evaluiert er den Ansatz, der als eine Verallgemeinerung von "Bounded Model Checking" gesehen werden kann. Die Implementierung wurde u.a. im Rahmen eines Model-Checking Wettbewerbs (RERS Challenge 2017) evaluiert und konnte in einer Kategorie alle Formeln korrekt lösen, was die Frage zur praktischen Anwendbarkeit letztendlich positiv beantwortet.

Die Arbeit wurde von Prof. Dr. Martin Leucker, Direktor des Instituts für Softwaretechnik und Programmiersprachen der Universität zu Lübeck, mit Unterstützung von Normann Decker ausgegeben und betreut.

Anton Pirogov, 1993 in Moskau geboren, legte sein Abitur in Hameln ab. 2012 – 2017 absolvierte er das Bachelor- und das Masterstudium der Informatik an der Universität zu Lübeck. Er war Tutor am Institut für Theoretische Informatik der Universität und  wissenschaftliche Hilfskraft am Max-Planck-Institut für Evolutionsbiologie in Plön beim Projekt „Entwicklung eines neuen Komplexitätsmaßes für DNA“. Aktuell ist er Doktorand an der Rheinisch-Westfälischen Technischen Hochschule (RWTH) Aachen am Lehrstuhl für In-formatik 7 „Logik und Theorie Diskreter Systeme“ und forscht im Bereich der Automatentheorie.

Hintergrund

Model Checking ist eine Methode zur Verifikation von (Software-)Systemen. Im Gegensatz zu dem in der Praxis bereits etablierten klassischen Testen von Software durch die Softwareentwickler funktioniert Model Checking vollautomatisch und liefert stärkere Korrektheitsgarantien.

Die erwünschten Eigenschaften werden mathematisch formuliert und von entsprechenden Model Checking Werkzeugen überprüft, wobei im Gegensatz zu gewöhnlichem Testen keine Testfälle mühselig vom Entwickler konstruiert werden müssen und keine Randfälle übersehen werden können. Falls die gewünschte Eigenschaft verletzt wird, liefert ein Model Checking Werkzeug auch üblicherweise ein Gegenbeispiel, was die Entwickler bei der anschließenden Fehlersuche unterstützt.

Da diese Verifikationstechnik in der Regel sehr rechenaufwendig ist, konnte sie lange nur zur Verifikation von kleineren Systemen oder kritischen Teilkomponenten verwendet werden. Durch stetige Weiterentwicklung und Verbesserung dieser Verifikationsmethode in der Wissenschaft wird Model Checking aber auch immer mehr für die Industrie interessant und wird u.a. in der Qualitätssicherung beim Entwurf großer integrierter Schaltungen eingesetzt.