Praktikum Programmanalyse WS24/25

Organisation

Im Wintersemester 2024/25 bietet das Institut für Theoretische Informatik das Praktikum Programmanalyse an. Das Ziel dieses Praktikums ist es, die Lerninhalte der Vorlesung Programmanalyse zu vertiefen.

• Zielgruppe des Praktikums sind Informatiker aus dem Bachelor- und Masterstudiengang.
• Bachelor Studenten beachten bitte, dass das Praktikum 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.
• Bei Interesse senden Sie bitte eine EMail an Jakob Tepe oder Jan Grünke
• 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.

• Kickoff ist am Donnerstag 17.10. um 15 Uhr im Raum IZ 358

Thema

Das Ziel des Praktikums ist es, formale Methoden zur Verifikation, welche in der Vorlesung Programmanalyse vorgestellt wurden, zu vertiefen. Insbesondere sollen ausgewählte Techniken implementiert werden.

Das tatsächliche Thema des Praktikums kann in Absprache mit den Teilnehmern erfolgen. Als vorläufiges Thema schlagen wir vor die CEGAR-Loop zu implementieren, um rekursive While-Programme auf Korrektheit zu überprüfen. Abhängig von der Teilnehmerzahl wird 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.