F: Stell dir vor du arbeitest in einer Firma und die anderen Programmierer machen zu viele ArrayIndexOutOfBoundsExceptions, der Boss sagt dass du die fixen sollst. Was tust du?
A: Finde mögliche AIOBE durch statische Analyse.
A: Erkläre kurz abstrakte Interpretation mit Intervallen
A: Erkläre kurz symbolische Ausführung
F: Wie konstruiert man die Pfadbedingung denn?
A: Kurze erklärung dazu
F: Aber wieso so kompliziert, die Variablen haben doch nur einen Wert, es wir doch am Ende nur ein Pfad durchlaufen?
A: Symbolische Ausführung durchläuft nicht für konkreten Wert, sondern gewissermaßen für alle möglichen Werte gleichzeitig.
F: Jetzt sagt der Boss aber dass die Verfahren entweder immer zu viele false positives haben oder zu viele false negatives. Er will dass du exakt die falschen Stellen findest und nur die.
A: Geht nicht, unentscheidbar wegen Halteproblem
F: Wo konkret?
A: Bei Schleifen und Rekursion
F: Bei Schleifen immer?
A: Wenn die Iterationszahl klar ist ist es kein Problem, nur wenn eine komplexe Schleifenbedingung vorhanden ist, dann müsste man eine Schleifeninvariante konstruieren