Seminar in Theoretical CS, Summer Semester 2017
News
- 13.01.2017: we are online
Deadlines
| 20.04.2017, 13:00 | Introduction at seminar room of i2 (building E1, room 4201b) |
| 15.05.2017 | Detailed outline of report due |
| 12.06.2017 | Seminar report due |
| 03.07.2017 | Presentation slides due |
| 17.07.2017, 09:00 | Seminar at seminar room of i2 (building E1, room 4201b) |
Overview
The term verification refers to theory and practice of computer-supported formal analysis methods for ensuring correctness of (hardware and) software systems. The modeling and verification of such systems is an important issue. In particular, safety-critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems. Testing can identify problems, especially if done in a rigorous fashion, but is generally not sufficient to guarantee a satisfactory level of quality.
To ensure the soundness of verification results, formal methods for analysing software on source-code level have been and are being developed, commonly referred to as Static (Program) Analysis. Related techniques such as data-flow analysis or abstract interpretation have originally 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 the related research activities of the MOVES group. It covers several areas of computer science to which computed-aided verification techniques and related analysis methods are central, and which represent the research fields of the respective supervisors. Each area features a number of topics which are described 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 semantics of programming languages, program analysis, model checking and/or concurrency theory is helpful but not mandatory
Topics
Pointer and Shape Analysis
- Fractional Permissions for Concurrency
- Literature: S. Heule, K.R.M. Leino, P. Müller, A.J. Summers: Fractional permissions without the fractions
- Supervisor: Christina Jansen
- Student: –
- Symbolic Permission Accounting
- Literature: Marieke Huisman, Wojciech Mostowski: A Symbolic Approach to Permission Accounting for Concurrent Reasoning
- Supervisor: Thomas Noll
- Student: Ricardo Marzulli
- Compositional Shape Analysis by means of Bi-Abduction
- Literature: Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, Hongseok Yang: Compositional Shape Analysis by means of Bi-Abduction
- Supervisor: Christina Jansen
- Student: –
- Amortised Resource Analysis
- Literature: Robert Atkey: Amortised Resource Analysis with Separation Logic
- Supervisor: Christoph Matheja
- Student: –
Advanced Model Checking Techniques
- Counterexample-Guided Abstraction Refinement
- Literature: Edmund Clarke et al.: Counterexample-Guided Abstraction Refinement
- Supervisor: Matthias Volk
- Student: Tom Janson
- Assume-Guarantee Reasoning
- Literature: Mihaela Gheorghiu Bobaru, Corina S. Păsăreanu, Dimitra Giannakopoulou: Automated Assume-Guarantee Reasoning by Abstraction Refinement
- Supervisor: Christian Dehnert
- Student: –
- Fairness
- Literature: Byron Cook, Heidy Khlaaf, Nir Piterman: Fairness for Infinite-State Systems
- Supervisor: Sebastian Junges
- Student: –
- Bounded Model Checking
- Literature: Armin Biere et al.: Bounded model checking
- Supervisor: TBA
- Student: –
- Configurable Software Verification
- Literature: Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Supervisor: Tim Lange
- Student: –
- IC3
- Literature: Arie Gurfinkel, Alexander Ivrii: Pushing to the Top
- Supervisor: Tim Lange
- Student: –
- Probabilistic Model Checking
- Literature: Ernst Moritz Hahn et al.: Lazy Probabilistic Model Checking without Determinisation
- Supervisor: Tim Quatmann
- Student: –
- Monte Carlo Model Checking
- Literature: Radu Grosu, Scott A. Smolka: Monte Carlo Model Checking
- Supervisor: Matthias Volk
- Student: –
- Concurrent Model Checking Algorithms
- Literature: Gavin Lowe: Concurrent depth-first search algorithms based on Tarjan’s Algorithm
- Supervisor: Matthias Volk
- Student: –
Analysis of Probabilistic Programs
- Sampling for Probabilistic Programs
- Literature: A.V. Nori, C.K. Hur, S.K. Rajamani, S. Samuel: R2: An Efficient MCMC Sampler for Probabilistic Programs
- Supervisor: Christoph Matheja
- Student: –
- Slicing Probabilistic Programs
- Literature: C.-K. Hur, A.V. Nori, S.K. Rajamani, S. Samuel: Slicing probabilistic programs
- Supervisor: Christoph Matheja
- Student: –
- Sampling Functions for Probability Distributions
- Literature: Park, S., Pfenning, F., Thrun, S.: A probabilistic language based on sampling functions
- Supervisor: Benjamin Kaminski
- Student: –
- Static Analysis of Probabilistic Programs
- Probabilistic Termination
- Literature: Annabelle McIver & Carroll Morgan: A New Rule for Almost-Certain Termination of Probabilistic- and Demonic Programs.
- Supervisor: Benjamin Kaminski
- Student: –
Additional Material
Registration
Registration to the seminar is handled between January 13 and 29, 2017, via the central online form. Later applications will not be considered.
Contact
Thomas Noll <noll at cs.rwth-aachen.de>