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 
• M2: Abstrakte Interpretation: Domains
• M3: Predicate Abstraction
• M4: Compositional Bounded Model Checking
• M5: Fuzzing
• M6: Delta-Debugging
• M7: Explicit-State Model Checking
• M8: Combinatorial Testing
• M9: Advanced Coverage Criteria
• M10: Softwarequalitäts-Standards
• M11: Symbolic Model Checking
• M12: Bounded Model Checking
• W1: Valgrind
• W2: Clang Static Analyzers
• W3: SonarQube
• W4: PMD
• W5: Frama-C
• W6: KeY
• W7: Polyspace
• W8: SMACK
• W9: SPIN

Literatur

Liste der Einstiegspaper kann hier heruntergeladen werden.

Die Folien der Auftaktveranstaltung finden Sie hier.

Hinweise für einen guten Seminarvortrag gibt es z.B. von Andreas Zeller oder Georg Schied et al.

Termine

• 25.10.2019: Vorbesprechung / Auftaktveranstaltung
• 08.11.2019: Themenvergabe
• 15.11.2019: Literaturbesprechung (Abgabe der erweiterten Literaturliste am 13.11.)
• 22.11.2019: Besprechung Gliederung und Kernthemen Gruppe "Methoden" (Abgabe der Gliederung am 20.11.)
• 29.11.2019: Besprechung Gliederung und Kernthemen Gruppe "Werkzeuge" (Abgabe der Gliederung am 27.11.)
• 06.12.2019: Besprechung erste Version Vortragsfolien Gruppe "Methoden" (Abgabe der Folien 04.12.)
• 13.12.2019: Besprechung erste Version Vortragsfolien Gruppe "Werkzeuge" (Abgabe der Folien  11.12.)
• 20.12.2019: Allgemeine Fragestunde
• 10.01.2020: Besprechung überarbeitete Version Vortragsfolien Gruppe "Methoden" (Abgabe der Folien am 08.01.)
• 17.01.2020: Besprechung überarbeitete Version Vortragsfolien Gruppe "Werkzeuge" (Abgabe der Folien am 15.01.)
• 24.01.2020: Allgemeine Fragestunde
• 31.01.2020: Besprechung Entwurf Ausarbeitung Gruppe "Methoden" (Abgabe vorläufige Version am 29.01.)
• 07.02.2020: Besprechung Entwurf Ausarbeitung Gruppe "Werkzeuge" (Abgabe der vorläufigen Version am 05.02.)
• Mi./Do. 19./20.02.2020: Vorträge, Industrievortrag

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. An den beiden Vortragstagen (19./20.02.) ist für alle Anwesenheitspflicht.

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.

Die Vorträge finden sowohl am Mittwoch als auch am Donnerstag in Seminarraum 131, Geb. 50.34 statt.

Mi. 19.02.2020

• Session 1 (Chair: D.G.)
  • 09:00-09:35: M1 Abstrakte Interpretation
  • 09:35-10:15: W7 Polyspace
• Pause
• Session 2 (Chair: A.S.)
  • 10:25-11:00: M12 Bounded Model Checking
  • 11:00-11:35: M4 Compositional Bounded Model Checking
  • 11:35-12:15: W9 Spin
• Pause
• Session 3 (Chair: A.L.)
  • 13:00-13:35: M5 Fuzzing
  • 13:35-14:10: M8 Combinatorial Testing
  • 14:10-14:45: M9 Advanced Coverage Criteria
• Pause
• Session 4 (Chair: Carsten Sinz)
  • 15:00-16:00: Industrievortrag Daimler (Udo Gleich, André Schmidt)

Do. 20.02.2020

• Session 5 (Chair: J.H.)
  • 09:00-09:35: M10 Software-Qualitätsstandards
  • 09:35-10:15: W3 SonarQube
  • 10:15-10:55: W4 PMD
• Pause
• Session 6 (Chair: J.M.)
  • 11:10-11:45: M6 Delta-Debugging
  • 11:45-12:25: W1 Valgrind
  • 12:25-13:05: W2 Clang Static Analyzers
     

Abgabe der Ausarbeitung

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

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.