Software-Zuverlässigkeit

1. Klassische Softwaretestverfahren
   • Äquivalenzklassen und Grenzwertanalyse
   • Codeüberdeckungsmaße
2. Systematisches Testen & Model Checking
   • Durchsuchung des Zustandsraums
   • Abstraktion: Modellierung
   • Modell und Implementierung
   • Praktikum: TLA+
3. Fuzzing & Symbolic Execution
   • Generierung von Testeingaben für eine hohe Codeüberdeckung mittels
   • a) Systematischer Mutation von Testeingaben: Greybox-Fuzzing
   • b) Lösung der Pfadbedingung: Symbolic Execution
   • Vor- und Nachteile beider Ansätze
   • Praktika: AFL++, Z3 SMT Solver, IntelliTest
4. Programmverifikation
   • Korrektheits- und Vollständigkeitsbeweise
   • Schleifeninvarianten
   • Praktikum: Dafny

Kapitel 1: Klassische Softwaretestverfahren:

• Kleuker, Qualitätssicherung durch Softwaretests
  • Kapitel 4 und 5
• Aniche, Effective Software Testing
  • Kapitel 2 und 3

Kapitel 2: Systematisches Testen & Model Checking

• Dokumentation des JavaPathFinders
  • What is JPF
  • Testing vs. Model Checking
• Kleuker, Formale Modelle der Softwareentwicklung
  
  • Kapitel 2
• Dokumentation TLA+
  • TLA+ Website

Kapitel 3: Fuzzing & Symbolic Execution

• The Fuzzing Book
  • Greybox Fuzzer
  • Concolic Fuzzer
  • Symbolic Fuzzer

Kapitel 4: Programmverifikation

• Kleuker, Formale Modelle der Softwareentwicklung
  • Kapitel 5
• K. Leino, Program Proofs