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 and
Languages group takes place on Wednesday, 6 March 2013, 1.00pm -
2.00pm p.m., in the lecture room EI4, 2nd floor, Gußhausstr. 25-29.

A specific pre-meeting for the lecture course LVA "Analysis and
Verification" and the first lecture take place on Tuesday, 5 March
2013, at 4.30pm in the " Hörsaal EI3a", 2nd floor, Gußhausstr. 25-29.

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.276 "Analysis and Verification"
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.