The language was changed to English.

Course Type (SWS)
Lecture: 3 │ Exercise: 1 │ Lab: 0 │ Seminar: 0
Exam Number: ZKD 59002
Type of Lecture:

Course with slides and blackboard

Language: German
Cycle: WS
ECTS: 6
Exam Type

Oral exam (30 minutes)

Oral Exam (30 min.)
Written Exam (120 min.)
assigned Study Courses
assigned People
assigned Modules
Information
Beschreibung:

Neben dem Einsatz auf dem Gebiet der Hardware-Verifikation halten Analyse- und Verifikationstechniken immer stärker Einzug in das Gebiet der Software-Verifikation.
Vor der Anwendung dieser Techniken ist es notwendig, das zu verifizierende System zu modellieren bzw. eine formale Semantik der zu behandelnden Programmiersprache anzugeben. Diese Vorlesung soll eine Einführung in die Gebiete Modellierung, Analyse und Verifikation geben.
Inhalte im Einzelnen:
1. Datenflussanalyse
- Fixpunkttheorie
- Monotone Frameworks
- Worklist-Algorithmus
- Anwendungsbeispiele: Compiler-Optimierung, Java Bytecode Verifier
2. Grundlagen der abstrakten Interpretation
- Galois-Verbindungen
- Sichere Approximation von Funktionen
- Abstraktionsverfeinerung

Lernziele:

Die Studierenden sollen Kenntnisse auf dem Gebiet der Verifikation und Analyse von Programmen erlangen. Dabei sollen sie Datenflussanalyse, deren Grundlagen (Fixpunkttheorie, monotone Frameworks) und ihre Anwendungen kennenlernen. Außerdem sollen sie Methoden aus dem Bereich der abstrakten Interpretation anwenden und deren Eignung für die Programmverifikation abschätzen können.

Literatur:

- Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis. Springer-Verlag, 1999.
- Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking. MIT Press, 2000.

Vorleistung:

Inhaltliche Voraussetzungen: Grundlagen der Automatentheorie und Logik

Infolink:
Bemerkung:
Description:

Apart from being used in the area of hardware verification, analysis and verification techniques are being increasingly applied in software verification. Before using such techniques, the system to be verified has to be modelled or the considered programming language has to be equipped with a formal semantics. This course will give an introduction into modelling, analysis and verification.
Topics in detail:
1. Data flow analysis
- Fixed-point theory
- Monotonous frameworks
- Worklist algorithm
- Application examples: compiler optimization, java bytecode verifier
2. Foundations of abstract interpretation
- Galois connections
- Safe approximation of functions
- Abstraction refinement

Learning Targets:

The students should gain knowledge about verification and analysis of programs. In particular they should get acquainted with data flow analysis, its foundations (fixed-point theory, monotonous frameworks) and its applications. Furthermore they should be able to apply methods from abstract interpretation and to evaluate their adequacy in program verification.

Literature:

- Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis. Springer-Verlag, 1999.
- Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking. MIT Press, 2000.

Pre-Qualifications:

Requirements: automata theory and logic

Info Link:
Notice: