Seminar in Theoretical CS, Winter Semester 2014/15
News
- 30.06.2014: we are online
Schedule
| 15.10.2014, 15:00 | Introduction at seminar room of i2 |
| -8 weeks | Table of contents due |
| -6 weeks | Preliminary version of report due |
| -4 weeks | Final version of report due |
| -2 weeks | Preliminary version of slides due |
| -1 week | Final version of slides due |
Overview
The term Computer-Aided Verification refers to theory and practice of computer-supported formal analysis methods for both 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.
Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of software. Due to the complexity of these approaches and the system they are applied to, automated computer support is indispensable.
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 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 (please refer to the references below). 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 and concurrency theory is helpful but not mandatory
Topics
(all presentations as “double features” on Thursdays 08:30-10:00 at I2 seminar room)
Axiomatic Verification
- Permission Accounting in Separation Logic
- Literature:
- Bornat, Calcagno, O’Hearn, Parkinson: Permission Accounting in Separation Logic
- O’Hearn: Introduction to Separation Logic
- Supervisor: Christina Jansen
- Student: Christoph Welzel
- Date: 08.01.2015
- Hoare-Style Verification of Graph Programs
- Literature:
- Supervisor: –
- Student: –
- Date: –
- Implicit Dynamic Frames
- Literature:
- Smans, Jacobs, Piessens: Implicit Dynamic Frames: Combining
Dynamic Frames and Separation Logic - O’Hearn: Introduction to Separation Logic
- Banerjee, Naumann, Rosenberg: Regional Logic
for Local Reasoning About Global Invariants - Supervisor: Christina Jansen
- Student: Tayfun Özen
- Date: 15.01.2015
Graph-Based Abstraction
- Grammar-Based Shape Analysis
- Literature:
- Supervisor: Thomas Noll
- Student: Jochen Schmücking
- Date: 22.01.2015
- Abstraction by Hyperedge Replacement Grammars
- Literature:
- Supervisor: Thomas Noll
- Student: Felix Bier
- Date: 22.01.2015
Inductive Incremental Verification
- Software Model Checking via IC3
- Literature:
- Supervisor: –
- Student: –
- Date: –
- IC3 Modulo Theories via Implicit Predicate Abstraction
- Literature:
- Supervisor: Tim Lange
- Student: Nico Friedrich
- Date: 05.02.2015
Verification of Probabilistic Systems
- Assume-Guarantee Reasoning
- Literature:
- Supervisor: Kevin van der Pol
- Student: Jonas Biel
- Date: 05.02.2015
- Analysis of Markov Decision Processes
- Literature:
- Supervisor: –
- Student: –
- Date: –
Additional Material
Registration
Registration to the seminar is handled between July 4 and 20, 2014, via the central online form.
Contact
Thomas Noll <noll at cs.rwth-aachen.de>