Static Methods for Quantitative Program Analysis (Seminar)

 Seminar in Theoretical CS, Winter 2018/19

News

  • 10.07.2018: we are online

Deadlines

10 Oct, 16:00 Kick-off meeting at seminar room of i2 (building E1, room 4201b)
5 Nov Detailed outline of report due
3 Dec Full report due
14 Jan Presentation slides due
29 Jan Seminar talks at seminar room of i2 (building E1, room 4201b; see  below for schedule)

Overview

Classical approaches to the formal analysis of software systems yield a Boolean answer: given a system and a property, the property either holds or is violated by the system. However, the notion of program correctness becomes blurred in the presence of numerical quantities such as execution times or probabilities of events in the system, the property, or both. As observed by Tom Henzinger in his article on Quantitative reactive modeling and verification, “the boolean partition of software into correct and incorrect programs falls short of the practical need to assess the behavior of software in a more nuanced fashion against multiple criteria.” This raises the need for formal approaches to analysing quantitative properties of software on source-code level, that is, for static methods supporting quantitative program analysis. Originally, static analysis techniques such as data-flow analysis or abstract interpretation have been designed for enabling code optimisation or highlighting possible coding errors. Nowadays, they are increasingly being employed for semantics-oriented activities such as proving software correctness.

The goal of this seminar is to give an overview of three research areas that constitute important application domains of quantitative methods: worst-case execution time analysis, heap resource analysis, and static analysis of probabilistic programs. Each area features a number of topics which are investigated in a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation.

Prerequisites

Basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic

Previous knowledge in formal semantics and static analysis of programming languages is helpful but not mandatory.

Schedule of Talks

Morning session
09:00-10:30 14, 2, 4
10:45-12:15 3, 6, 11
Afternoon session
14:00-15:00 5, 15

Topics

(The label “[B]” refers to topics that are particularly suited for BSc students.)

Worst-Case Execution Time Analysis

  1. Timing Analysis by Integer Linear Programs [B]
  2. Timing Analysis by Abstract Segment Trees [B]
  3. Power-Aware Worst Case Execution Time Analysis [B]
  4. Timing Analysis by Abstract Interpretation
  5. Semantics-Based Worst Case Execution Time Analysis

Heap Resource Analysis

  1. Introduction to Separation Logic [B]
  2. Reasoning about Complexity of Data Structure Operations [B]
  3. Permission Accounting for Concurrent Threads [B]
  4. Graph-Based Reasoning about Relational Properties of Data Structures [B]
  5. Variables as Resources [B]
  6. Dataflow Analysis for Quantitative Properties of Tree Data Structures

Static Analysis of Probabilistic Programs

  1. Quantitative Separation Logic [B]
  2. Abstract Interpretation of a Probabilistic λ-Calculus [B]
  3. Estimating Probabilities of Program Assertions [B]
  4. Static Quantitative Reliability Analysis [B]
  5. Probabilistic Invariants and Almost-Sure Termination [B]
  6. Abstract Interpretation of Imperative Probabilistic Programs I
  7. Abstract Interpretation of Imperative Probabilistic Programs II

Additional Material

Registration

Registration to the seminar is organised via a central application procedure. Belated registrations are not possible.

Contact

Thomas Noll <noll at cs.rwth-aachen.de>