The participants acquire a profound theoretical and practical
understanding of fundamental concepts and principles of program
analysis, verification, and transformation which enables them to apply
techniques and tools resting on them competently and adequately, and
to well-groundedly assess the strengths and limitations of approaches
to program analysis, verification, and transformation, in particular
of automatic ones.

The course is concerned with concepts and principles of basic and
advanced approaches for the analysis and verification of software
systems with a focus on the concepts of soundness, completeness, and
optimality in analysis, verification and transformation. The lecture
part of the course stretches from Hoare logics to program and data
flow analysis, to the theory of abstract interpretation and to
model-checking. Regularly assigned exercises of the tutorial part of
the course give a hands-on experience of applying the various concepts
and principles and approaches based on them to problems and examples
that are mostly taken from the field of optimizing and verifying
compilation.

Part I: Motivation

• Basics
• Operational Semantics of WHILE
• Denotational Semantics of WHILE
• Axiomatic Semantics of WHILE
• Worst-Case Execution Time Analysis

Part II: Analysis and Verification

• Program Analysis
• Program Verification vs. Program Analysis
• Reverse Data Flow Analysis
• Chaotic Fixed Point Iteration
• Basic Block vs. Single Assignment Graphs

Part III: Transformation and Optimality

• Elimination of partially dead Assignments
• Elimination or partially redundant Assignments
• Combining PRAE and PDCE
• Constant Folding on the Value Graph

Part IV: Abstract Interpretation and Model-Checking

• Abstract Interpretation and DFA
• Modell-Checking and DFA

Part V: Conclusions and Prospectives

• Summary and Prospectives

[ A joint pre-meeting for all courses offered by the Compilers andLanguages group tentatively takes place on Wednesday, 4 March 2015, 1.00pm -
2.00pm p.m., in the lecture room EI4, 2nd floor, Gußhausstr. 25-29. (Cancelled for SS 2015) ]

A specific pre-meeting for the lecture course LVA "Analysis and
Verification" and the first lecture take place on Tuesday, 3 March
2015, at 4.30pm in the "Library E185.1, Argentinierstr. 8, 4th floor (centre).

ECTS Break Down:

The course is assigned 3.0 ECTS points. This corresponds to an average
workload of 75 hours. This average workload is divided among the
various parts of the course as follows:

• Attending the lectures, pre- and post-processing: 35 hours.
• Assignments: 30 hours.
• Preparation for the examination and oral examination: 10 hours.

Grading of assignments and an oral examination. The final grade is
composed of the grades of the regular assignments (50%) and the grade
of the final oral examination (50%).

Basic knowledge in theoretical computer science and programming are
mandatory. Basic knowledge of compiler construction as e.g. imparted
by the courses 185.A48 VU 4.0h "Compilers" or 185.A04 VU 2.0
"Optimizing Compilers are useful but not strictly obligatory.

The course complements the courses 185.A04 "Optimizing Compilers"
und 185.A56 "Semantics of Programming Languages." The course is thus
especially recommended for students who want to specialize in the
field of programming languages and compilers and to write e.g. a seminar
or master thesis in these fields.