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 |

### 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.

### Topics

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

#### Worst-Case Execution Time Analysis

- Timing Analysis by Integer Linear Programs [B]
**Literature:**R. Wilhelm: Determining bounds on execution times. Handbook on Embedded Systems, 2005**Literature:**Y.-T. Steven Li, S. Malik, A. Wolfe: Efficient Microarchitecture Modeling and Path Analysis for Real-Time Software. RTSS 1995**Supervisor:**–**Student:**–

- Timing Analysis by Abstract Segment Trees [B]
**Literature:**P. Černý, T.A. Henzinger, L. Kovács, A. Radhakrishna, J. Zwirchmayr: Segment Abstraction for Worst-Case Execution Time Analysis. ESOP 2015**Supervisor:**Benjamin Kaminski**Student:**Lena Verscht

- Power-Aware Worst Case Execution Time Analysis [B]
**Literature:**W. Bao, S. Tavarageri, F. Ozguner, P. Sadayappan: PWCET: Power-Aware Worst Case Execution Time Analysis. ICPP 2014**Supervisor:**Thomas Noll**Student:**Alexander Lüpges

- Timing Analysis by Abstract Interpretation
**Literature:**Jan Gustafsson, Andreas Ermedahl, Christer Sandberg, Bjorn Lisper: Automatic Derivation of Loop Bounds and Infeasible Paths for WCET Analysis Using Abstract Execution. RTSS 2006**Supervisor:**Benjamin Kaminski**Student:**Alex Hoppen

- Semantics-Based Worst Case Execution Time Analysis
**Literature:**J. Henry, M. Asavoae, D. Monniaux, C. Maïza: How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. LCTES 2014**Supervisor:**Thomas Noll**Student:**Christopher Brix

#### Heap Resource Analysis

- Introduction to Separation Logic [B]
**Literature:**P. O’Hearn: A Primer on Separation Logic. Marktoberdorf 2012**Supervisor:**Christoph Matheja**Student:**Christine Thomas

- Reasoning about Complexity of Data Structure Operations [B]
**Literature:**R. Atkey: Amortised Resource Analysis with Separation Logic. ESOP 2010**Supervisor:**–**Student:**–

- Permission Accounting for Concurrent Threads [B]
**Literature:**R. Bornat, C. Calcagno, P. O’Hearn, M. Parkinson: Permission accounting in separation logic. POPL 2005**Supervisor:**–**Student:**–

- Graph-Based Reasoning about Relational Properties of Data Structures [B]
**Literature:**H. Arndt, C. Jansen, C. Matheja, T. Noll: Graph-Based Shape Analysis Beyond Context-Freeness. SEFM 2018**Supervisor:**Christoph Matheja**Student:**–

- Variables as Resources [B]
**Literature:**M. Parkinson, R. Bornat, C. Calcagno: Variables as Resource in Hoare Logics. LICS 2006**Supervisor:**–**Student:**–

- Dataflow Analysis for Quantitative Properties of Tree Data Structures
**Literature:**R. Rugina: Quantitative Shape Analysis. SAS 2004**Supervisor:**Christoph Matheja**Student:**Eric Maßelter

#### Static Analysis of Probabilistic Programs

- Quantitative Separation Logic [B]
**Literature:**K. Batz, B.L. Kaminski, J.-P. Katoen, C. Matheja, T. Noll: Quantitative Separation Logic. arXiv 2018**Supervisor:**–**Student:**–

- Abstract Interpretation of a Probabilistic λ-Calculus [B]
**Literature:**A. Di Pierro, C. Hankin, H. Wiklicky: Probabilistic λ-calculus and Quantitative Program Analysis. JLC 2005**Supervisor:**–**Student:**–

- Estimating Probabilities of Program Assertions [B]
**Literature:**S. Sankaranarayanan, A. Chakarov, S. Gulwani: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. PLDI 2013**Supervisor:**Benjamin Kaminski**Student:**Jan Fritz

- Static Quantitative Reliability Analysis [B]
**Literature:**M. Carbin, S. Misailovic, M.C. Rinard: Verifying quantitative reliability for programs that execute on unreliable hardware. CACM 2016**Supervisor:**Thomas Noll**Student:**Esther Tala

- Probabilistic Invariants and Almost-Sure Termination [B]
**Literature:**A. Chakarov, S. Sankaranarayanan: Probabilistic Program Analysis with Martingales. CAV 2013**Supervisor:**–**Student:**–

- Abstract Interpretation of Imperative Probabilistic Programs I
**Literature:**D. Monniaux: Abstract Interpretation of Probabilistic Semantics. SAS 2000**Supervisor:**–**Student:**–

- Abstract Interpretation of Imperative Probabilistic Programs II
**Literature:**P. Cousot, M. Monerau: Probabilistic abstract interpretation. ESOP 2012**Supervisor:**–**Student:**–

### Additional Material

- Introductory slides
- Report template
- Presentation template
- How to write scientific papers
- How to give presentations
- Introduction to LaTeX

### 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>