VU Analyse und Verifikation

Exam informations

Beurteilung von Beispielen und mündliche Prüfung. Die Gesamtnote setzt
sich je zur Hälfte aus der Übungsnote auf die Beispiele und der Note
für die mündliche Prüfung zusammen.

Workload for exams

Description

Die Studierenden erhalten ein profundes theoretisches und praktisches
Verständnis fundamentaler Prinzipien und Konzepte in Programmanalyse,
-verifikation und -transformation, das sie befähigt, darauf gegründete
Verfahren kompetent und adäqat anzuwenden und die Möglichkeiten und
Grenzen insbesondere automatischer Verfahren zur Programmanalyse,
-verifikation und transformation fundiert einzuschätzen und zu
beurteilen.

Die Vorlesung beschäftigt sich mit Konzepten und Prinzipien
grundlegender und fortgeschrittener Verfahren zur Analyse und
Verifikation von Softwaresystemen. Im Mittelpunkt stehen dabei die
Konzepte von Korrektheit, Vollständigkeit und Optimalität in Analyse,
Verifikation und Transformation. Die Vorlesung spannt dabei den Bogen
von Hoarescher Logik über Programm- und Datenflussanalyse zur
Theorie abstrakter Interpretation und Modellprüfung. Illustrierende
Transformationen werden dabei besonders dem Bereich optimierender und
verifizierender Übersetzung entnommen. Anhand regelmäßig gestellter
Übungsaufgaben werden die in der Vorlesung behandelten Themen an
maßgeschneiderten Aufgabenstellungen erprobt und angewendet.

Teil I: Motivation

  • Grundlagen
  • Operationelle Semantik von WHILE
  • Denotationelle Semantik von WHILE
  • Axiomatische Semantik von WHILE
  • Worst-Case Execution Time Analyse

Teil II: Analyse und Verifikation

  • Programmanalyse
  • Programmverifikation vs. Programmanalyse
  • Reverse Datenflussanalyse
  • Chaotische Fixpunktiteration
  • Basisblock- vs. Einzelanweisungsgraphen

Teil III: Transformation und Optimalität

  • Elimination partiell toter Anweisungen
  • Elimination partiell redundanter Anweisungen
  • Kombination von PRAE und PDCE
  • Konstantenfaltung auf dem Wertegraphen

Teil IV: Abstrakte Interpretation und Modellprüfung

  • Abstrakte Interpretation und DFA
  • Modellprüfung und DFA

Teil V: Abschluss und Ausblick

  • Resümee und Perspektiven




  • LVA-Nummer: 185.276
  • ECTS: 3.0
  • Stunden: 2

Module

Lecturers

Examples

Möchtest du die Beispiele bewerten musst du dich einloggen. Derzeit funktioniert das über Facebook, wir arbeiten an einem Login über TISS! Facebook Login

Download all as ZIP File
Add files...