Das Proseminar gibt eine Einführung in verschiedene Werkzeuge und Methoden der Software-Analyse. Software-Analysen haben zum Ziel, Fehler automatisiert zu finden (Bug Finding) oder deren Abwesenheit zu beweisen (Verifikation). Anhand einzelner Vorträge sollen verschiedene Werkzeuge und Methoden zur automatisierten Fehlersuche für eine Reihe von Programmiersprachen vorgestellt werden. Vorträge bestehen entweder aus der Präsentation einer Methode zur Programm-Analyse oder der Vorstellung eines Werkzeugs, wobei in letzterem Fall auch eine Beschreibung der dahinterstehenden theoretischen Methode sowie einfache Anwendungsbeispiele im Vortrag enthalten sein sollen.

Themen

• M1: Abstrakte Interpretation: Grundlagen  Holger Klein
• M2: Abstrakte Interpretation: Domains  Paul Reichert
• M3: Predicate Abstraction  Tobias Telge
• M4: Counterexample-Guided Abstraction Refinement  Thomas Caspers
• M5: Fuzzing  Philipp Krüger
• M6: Delta-Debugging  Moritz Laupichler
• M7: Explicit-State Model Checking  Marc Jepsen
• M8: Combinatorial Testing  Etienne Brunner
• M9: Advanced Coverage Criteria  Stephan Bohr
• M10: Softwarequalitäts-Standards  Nicole Gerhardt
• M11: Symbolic Model Checking  Pierre Bonert
• M12: Bounded Model Checking  ---
• W1: Valgrind  Jonathan Schenkenberger
• W2: Clang Static Analyzers  Le Yang
• W3: SonarQube  Dennis Loran
• W4: PMD  Sajjad Ahmad
• W5: Frama-C  Dimitri Kuklev
• W6: KeY  Martin Wittlinger
• W7: Polyspace  Houraalsadat Mortazavi Moshkenan
• W8: SMACK  Patrick Deubel
• W9: SPIN  ---

Literatur

Liste der Einstiegspaper kann hier heruntergeladen werden.

Die Folien der Auftaktveranstaltung finden Sie hier.

Termine

• 15.10.2018: Vorbesprechung / Auftaktveranstaltung
• 19.10.2018: Allgemeine Fragestunde
• 26.10.2018: Literaturbesprechung Gruppe "Methoden" (Abgabe der erweiterten Literaturliste am 24.10.)
• 02.11.2018: Literaturbesprechung Gruppe "Werkzeuge" (Abgabe der erweiterten Literaturliste am 31.10.)
• 09.11.2018: Besprechung Gliederung und Kernthemen Gruppe "Methoden" (Abgabe der Gliederung am 05.11.)
• 16.11.2018: Besprechung Gliederung und Kernthemen Gruppe "Werkzeuge" (Abgabe der Gliederung am 12.11.)
• 23.11.2018: Allgemeine Fragestunde
• 30.11.2018: Besprechung erste Version Vortragsfolien Gruppe "Methoden" (Abgabe der Folien 26.11.)
• 07.12.2018: Besprechung erste Version Vortragsfolien Gruppe "Werkzeuge" (Abgabe der Folien  03.12.) [Termin ausnahmsweise 15:30-17:00 in Seminarraum -120]
• 14.12.2018: Besprechung überarbeitete Version Vortragsfolien Gruppe "Methoden" (Abgabe der Folien am 10.12.2018)
• 21.12.2018: Besprechung überarbeitete Version Vortragsfolien Gruppe "Werkzeuge" (Abgabe der Folien am 17.12.2018)
• 11.01.2019: Allgemeine Fragestunde
• 18.01.2019: Besprechung Ausarbeitung Gruppe "Methoden" (Abgabe vorläufige Version am 14.01.2019)
• 25.01.2019: Besprechung Ausarbeitung Gruppe "Werkzeuge" (Abgabe der vorläufigen Version am 21.01.2019)
• Fr. 01.02.2019: Industrievortrag: Dr. Hendrik Post, Robert Bosch GmbH, Stuttgart, Centre of Competence for Software Verification and Validation (14 Uhr, Seminarraum 131)
• Fr. 01.02.2019: Vorträge Gruppe "Methoden" (15-18 Uhr, Seminarraum 131)
• Fr. 08.02.2019: Vorträge Gruppe "Methoden" (13-18 Uhr, Seminarraum 131)
• Mo. 11.02.2019: Vorträge Gruppe "Werkzeuge" (9-15 Uhr, Seminarraum 236)

Abgaben haben zum angegebenen Stichtag per E-Mail zu erfolgen.

Die Teilnahme an den Terminen der eigenen Gruppe sind verpflichtend, die der anderen Gruppe sind freiwillig.

Vorträge

Vorträge sollen maximal 25 Minuten lang sein. Bitte achten Sie dringend darauf, diese Zeit einzuhalten! Vorträge der Gruppe "Werkzeuge" dürfen optional eine Tool-Präsentation enthalten. Dann ändert sich die Vortragszeit auf maximal 20 Minuten plus 10 Minuten für die Tool-Präsentation. Nach jedem Vortrag ist eine Diskussion von 5-10 Minuten vorgesehen.

Fr. 01.02.2019 (Seminarraum 131):

• 14:00-15:00: Industrie-Vortrag: Dr. Hendrik Post, Robert Bosch GmbH
• Pause
• 15:25-16:00: M1  Abstrakte Interpretation: Grundlagen (HK)
• 16:00-16:35: M2  Abstrakte Interpretation: Domains (PR)
• Pause
• 16:50-17:25: M4  Counterexample-Guided Abstraction Refinement (TC)
• 17:25-18:00: M9  Advanced Coverage Criteria (SB)

Fr. 08.02.2019 (Seminarraum 131):

• 13:00-13:35: M3  Predicate Abstraction (TT)
• 13:35-14:10: M11  Symbolic Model Checking (PB)
• Kaffeepause
• 14:25-15:00: M6  Delta-Debugging (ML)
• 15:00-15:35: M7  Explicit-State Model Checking (MJ)
• 15:35-16:10: M8  Combinatorial Testing (EB)
• Kaffeepause
• 16:25-17:00: M10  Software-Qualitätsstandards (NG)
• 17:00-17:35: M5  Fuzzing (PK)

Mo. 11.02.2019 (Seminarraum 236):

• 09:00-09:40: W1  Valgrind (JS)
• 09:40-10:20: W2  Clang Sanitizers (LY)
• 10:20-11:00: W3  SonarQube (DL)
• Kaffeepause
• 11:15-11:55: W4  PMD (SA)
• 11:55-12:35: W5  Frama-C (DK)
• Mittagspause
• 13:00-13:40: W6  KeY (MW)
• 13:40-14:20: W7  Polyspace (HMM)
• 14:20-15:00: W8  SMACK (PD)

Abgabe der Ausarbeitung

Die Abgabe der Ausarbeitung erfolgt als PDF-Datei per E-Mail. Abgabgeschluss ist Freitag, der 22.03.2019.

Vorlagen

Ihre Ausarbeitung sollte einen Umfang von 10-15 Seiten haben und in LaTeX erstellt sein. Verwenden Sie dazu den LaTeX-Style des Leibniz-Zentrums für Informatik. Die Vorlage sowie ein Beispieldokument können Sie auf der Webseite https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/ herunterladen. Verwenden Sie das Format lipics-v2018/19-authors mit den Einstellungen \nolinenumbers und \hideLIPIcs (siehe dazu auch das Beispieldokument der Vorlage). \ArticleNo setzen Sie bitte auf das Kürzel Ihres Themas.