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
• Language WHILE
• Operational Semantics
• Denotational Semantics
• Axiomatic Semantics
• Axiomatic Execution Time Analysis

Part II: Analysis and Verification

• Program Analysis
• Reverse Program Analysis
• Parallel Program Analysis
• Program Verification vs. Program Analysis

Part III: Transformation and Optimality

• Chaotic Fixed Point Iteration
• Partially Dead and Faint Assignments
• Partially Redundant Assignments
• Partially Redundant Expressions
• Combined Transformations
• Constant Analysis on the Value Graph

Part IV: Abstract Interpretation and Model-Checking

• Abstract Interpretation and DFA
• ModelßChecking and DFA
• Model-Checking and Abstract Interpretation

Part V: Conclusions and Prospectives

• Summary and Prospectives

References

Appendix

• Mathematical Foundations
• Pragmatics: Flow Graph Variants

The preliminary course meeting and the first lecture takes
place on Wednesday, 6 March 2019, from 4.15pm to 5.45pm in
"Hörsaal EI3a, Elektrot.Institutsg. (2nd floor)," Gußhausstr. 25-29.

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.