After successful completion of the course, students are able to (among others)

• highlight, explain, and illustrate fundamental principles, concepts, and methods for program analysis and program verification, in particular, correctness and completeness of axiomatic semantics, data flow analysis, abstract interpretation, and model-checking.
• transfer and apply these concepts and methods to program transformation/optimization.
• understand and carve out commonalities and differences between program analysis and program verification.
• to realize, evaluate, and assess the potential and limitations of automatic and semi-automatic procedures for program analysis, program verification, and program transformation/optimization in the field of tension of decidability, scalability, efficacy, and usefulness.

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 Variant

Selected Reading Recommendations

• Beatrice Berard, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Peit, Laure Petrucci, Philippe Schnoebelen with Pierre McKenzie. Systems and Software Verification: Model-Checking Techniques and Tools. Springer- V., 2001.
• Jacques Loeckx, Kurt Sieber. The Foundations of Program Verification. Wiley, 1984.
• Flemming Nielson, Hanne Riis Nielson, Chris Hankin. Principles of Program Analysis. Springer-V., 2nd edition, 2005.
• Hanne Riis Nielson, Flemming Nielson. Semantics with Applications: An Appetizer. Springer-V., 2007.

Guided self-dependent learning and practicing (in-person in principle): guided by means of lecture and flipped classroom sessions, the self-dependent learning and practicing of the competencies described in the learning outcomes utilizing lecture notes, exercises, and further self-reliantly chosen material from text books, tutorials, and scientific articles proposed for further reading.

1. Role model and feedback-oriented learning (in-person in principle): Presenting, explaining, comparing, contrasting, and rating own and others solutions of assignments in tutor-guided tutorials.
2. Self-assessment tests (online and offline, no physical presence): Tests supporting the regular self-assessment and self-reflection of one's own previous progress and success of learning; additional central and control questions.

The lecture course is planned in principle with in-person meetings. In case that this is not or no longer be possible due to new COVID-19 restrictions, the lecture course will be continued online (Zoom) in terms of real-time video conferences in order to preserve the advantages of the directness of in-person course meetings to the largest possible extent.

ECTS Break Down:

The course is assigned 3.0 ECTS points. This corresponds to an average
workload of 75 hours. This average workload is split among the
various learning activities of the course as follows (the notions Part I to Part VI refer to the respective parts of the course notes):

• Guided learning activities (in-person in principle, 17.5h)
• Lecture: 12.0h (12 units * 1.0h)
• Flipped classroom: 3.0h (6 units * 0.5h)
• Tutorials: 2.5h (5 units * 0.5h)
• Independent learning activities (studying from home, 57.0h)
• Autonomous acquirement of learning outcomes: 35.0h (Guide value: Part I/4.0h, Part II/6.0h, Part III/10.0h, Part IV/10.0h, Part V/4.0h, Part VI/1.0h)
• In particular: Solving assignments: 20.0h (Guide value: 4 Assignments * 2.0h + 4 Assignments * 3.0h)
• Oral exam preparation (in-person in principle): 2.0h
• Oral exam: 0.5h

The course starts with a preliminary course meeting and the first lecture
on Wednesday, 1 March 2023, 4.15pm to 5.45pm, Seminarraum FAV 01 A.

• Online/offline, without physical presence: Eight rated submissions of assignments.
• In person in principle: One rated 30 minute oral examination.

There are no other rated assessments.

Required technical equipment: Stable Internet connection, internet connectable device with audio/video receiver and transmitter.

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.