Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

Praktikum: Programmanalyse

Sommersemester 2019

Organisation

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

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:

Einige der obigen Punkte setzen die Verwendungen eines SAT-Solvers bzw. SMT-Solvers voraus. Microsoft Z3 ist ein solches Tool.

Ansprechpartner

Betreut wird das Projekt durch Roland Meyer und Sebastian Wolff. Bei Fragen wenden Sie sich bitte an Sebastian.