Theoretical Computer Science

Project

Summer Term 2021

News

15. April

Das Kickoff-Meeting zum Projekt findet am Montag, den 26.04 um 10:00 Uhr über BigBlueButton statt.

19. März

Die Informationen auf dieser Seite sind noch vorläufig.

Organisation

Im Sommersemester 2021 bietet das Institut für Theoretische Informatik ein Projekt (Praktikum) an. Das Projekt thematisiert die Verifkation und vertieft die am Institut unterrichteten Techniken das Implementieren eines Verifikations-Tools. Ein Beispiel-Thema findet sich unten.

In Absprache mit den Teilnehmern, kann das Projekt sowohl als Teamprojekt als auch als Praktikum Programmanalyse eingebracht / anerkannt werden.

• Zielgruppe des Praktikums sind Informatiker aus dem Bachelor- und Masterstudiengang.
• Bachelor Studenten beachten bitte, dass das Praktikum Programmanalyse als Masterveranstaltung im Modulhandbuch gelistet ist. Klären Sie bitte rechtzeitig mit dem Prüfungsamt ab, unter welchen Bedingungen Sie die Veranstaltung in ihr Bachelorstudium einbringen können.
• Es werden regelmäßige Treffen erfolgen, in denen der aktuelle Stand und das weitere Vorgehen besprochen werden. Ort und Raum sowie Intervall der Treffen wir im Kickoff-Meeting festgelegt.

Beispiel-Thema

Ein mögliches Thema ist die Implementierung der CEGAR-Loop, um rekursive While-Programme auf Korrektheit zu überprüfen (vgl. Vorlesung Programmanalyse). Abhängig von der Teilnehmerzahl kann das Thema ggf. um Pointer-Analysen und/oder IC3 erweitert.

Vorläufige CEGAR-Loop:

• Eingabe: Boogie-Programm. (Boogie ist eine relativ simple Intermediate-Verifikationssprache von Microsoft Research. Es existieren Tools, um z.B. LLVM IR in Boogie-Programme zu übersetzten. Damit ist es also prinzipiell möglich, C/C++ Programme als Input für den zu entwickelnden Model-Checker zu verwenden.) Zum parsen solcher Programme kann z.B. AntLR verwendet werden.
• Berechnen der abstrakten Transitionsrelation unter Verwendung der Prädikatenabstraktion, wie sie in der Vorlesung Programmanalyse vorgestellt wurde. Die Transitionsrelation soll symbolisch, d.h. als logische Formel, dargestellt und gespeichert werden. Dies kann in zwei Schritten geschehen:
  1. Abstraktion des Int-Programms in ein Bool-Programm. (Die Variablen des Bool-Programms sind dann die Prädikate der Abstraktion.)
  2. Übersetzen des Bool-Programms aus dem vorherigen Schritt in die abstrakte Transitionsrelation. (Hier sind Procedure-Summaries von Nöten, um rekursive Funktionen zu unterstützen.)
  Siehe Ball et al.: Automatic Predicate Abstraction of C Programs.
• Erreichbarkeitsanalyse: prüfe, ob ein/der bad state unter der abstrakten Transitionsrelation erreichbar ist. Als Verfahren soll IC3 zum Einsatz kommen, da es mit der symbolischen Darstellung der Transitionsrelation arbeiten kann. Siehe Bradley: SAT-Based Model Checking Without Unrolling.
• Extraktion eines Gegenbeispiels aus der Erreichbarkeitsanalyse. (Effizient aus der Liste der proof obligations von IC3.)
• Prüfen des Gegenbeispiels auf Echtheit. Falls es sich um ein echtes Beispiel handelt, soll dem Benutzer eine Erklärung, also Eingabedaten und ein Ablauf des Programms, geliefert werden. Hier kann z.B. ein Hoare-Beweis geführt werden. Für bessere Performanz sollte allerdings die Technik aus der folgenden Abstraktionsverfeinerung verwendet werden.
• Verfeinern der Abstraktion: aus dem unechten Gegenbeispiel sollen neue Prädikate berechnet werden. Siehe Henzinger et al.: Abstractions from Proofs.

Einige der obigen Punkte setzen die Verwendungen eines SAT-Solvers bzw. SMT-Solvers voraus. Microsoft Z3 ist ein solches Tool.