185.276 Analysis and Verification
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2021S, VU, 2.0h, 3.0EC, to be held in blocked form
TUWEL

Properties

  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise
  • Format: Distance Learning

Learning outcomes

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.

Subject of course

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.

Teaching methods

Holding Mode: Online

According to current COVID-19 restrictions and directives of the vice rectorate for academic affairs and the dean's office of academic affairs from January 26 abd January 31, 2021, the lecture course 185.276 Analysis and Verification is exclusively held online. The advantages of the directness of face-to-face course meetings shall be preserved to the largest possible extent. All course meetings will thus be held as real-time video conferences.

  1. Guided self-dependent learning and practicing (online only): 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.
  2. Role model and feedback-oriented learning (online only): Presenting, explaining, comparing, contrasting, and rating own and others solutions of assignments in tutor-guided tutorials.
  3. 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.

Mode of examination

Immanent

Additional information

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 (exclusively online, 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 (exclusively online, video presence): 2.0h
  • Oral exam: 0.5h

The course starts with a preliminary course meeting and the first lecture
on Wednesday, 4 March 2020, 4.15pm to 6pm (inclusive of a 15min break) via Zoom. The Zoom-Link has been posted as a TISS message on 1 March 2021; it can also be found on the news board for course news in TISS and in the complementary TUWEL course.

Lecturers

Institute

Examination modalities

  • Online/offline, without physical presence: Eight rated submissions of assignments.
  • Online, face-to-face video presence: One rated 30 minute oral examination (consensually, the oral exam can be replaced by an equivalent oral exam on-site, if the then valid COVID rules should allow this).

There are no other rated assessments.

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

Course registration

Begin End Deregistration end
29.01.2021 01:00 12.03.2021 12:00 26.03.2021 23:59

Curricula

Literature

No lecture notes are available.

Previous knowledge

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.

Preceding courses

Accompanying courses

Continuative courses

Miscellaneous

Language

German