Trends in Computer-Aided Verification
Seminar in Theoretical CS, Winter Semester 2013/14
News
- 28.06.2013: Setup of this web page
- 11.10.2013: Topic distribution finished
Schedule
Wed 09.10.2013 15:30 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
(relative to date of presentation)
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.
Topics
(regular date: Monday 16:00-17:30 at I2 seminar room; except for 13.01.2014)
Verification of Pointer-Manipulating Programs
(supervisor: Christina Jansen)
- Alexey Gotsman, Josh Berdine, and Byron Cook: Interprocedural Shape Analysis with Separated Heap Abstractions
- Student: -
- Date: -
- Arend Rensink and Eduardo Zambon: Pattern-Based Graph Abstraction
- Student: -
- Date: -
Verification of Probabilistic Systems
(supervisor: Christian Dehnert)
- Krishnendu Chatterjee and Jakub Łącki: Faster Algorithms for Markov Decision Processes with Low Treewidth
- Student: Henrik Barthels
- Date: 09.12.2013
- Marta Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu: Assume-guarantee verification for probabilistic systems
- Student: Dustin H?tter
- Date: 09.12.2013
- Vojtech Forejt, Marta Kwiatkowska, and David Parker: Pareto Curves for Probabilistic Model Checking
- Student: Jens Katelaan
- Date: 16.12.2013
- Marta Kwiatkowska, Gethin Norman, and David Parker: Stochastic Games for Verification of Probabilistic Timed Automata
- Student: David Laukamp
- Date: 16.12.2013
- Holger Hermanns, Bj?rn Wachter, Lijun Zhang: Probabilistic CEGAR
- Student: Jan Uthoff
- Date: 06.01.2014
Model Checking with State-Space Abstractions
(supervisor: Tim Lange)
- Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani: Software model checking via large-block encoding
- Student: Thomas Mertens
- Date: 13.01.2014 at 15:15
- Aaron R. Bradley and Zohar Manna: Checking Safety by Inductive Generalization of Counterexamples to Induction
- Student: -
- Date: -
Formal Approaches to Testing
(supervisor: Sabrina von Styp)
- Machiel van der Bijl, Arend Rensink, and Jan Tretmans: Action Refinement in Conformance Testing
- Student: Kevin Jahns
- Date: 13.01.2014
- Ylies Falcone, Jean-Claude Fernandez, Thierry Jeron, Herve Marchand, and Laurent Mounier: More Testable Properties
- Student: Sascha M?ller
- Date: 13.01.2014
- Camille Constant, Thierry Jeron, Herve Marchand, and Vlad Rusu: Integrating Formal Verification and Conformance Testing for Reactive Systems
- Student: -
- Date: -
Analysis of Timed Systems
(supervisor: Harold Bruintjes)
- Jonas Rinast and Sybille Schupp: Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics
- Student: Christopher Kugler
- Date: 20.01.2014
- Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuh舫?er: Quantitative Timed Analysis of Interactive Markov Chains
- Student: Frederick Prinz
- Date: 20.01.2014
Interpolation-Based Model Checking
(supervisor: Viet Yen Nguyen)
- K.L. McMillan: Applications of Craig Interpolants in Model Checking
Vijay D担ilva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher: Interpolant Strength- Student: Christof Mroz
- Date: 27.01.2014
Program Synthesis
(supervisor: Kevin van der Pol)
- Andrew Ireland and Jamie Stark: Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis
- Student: Marcel Nehring
- Date: 27.01.2014
Information Flow Security
(supervisor: Thomas Noll)
- Stephen Chong and Ron van der Meyden: Using Architecture to Reason About Information Security
- Student: Thomas Henn
- Date: 03.02.2014
- Michael R. Clarkson and Fred B. Schneider: Hyperproperties
- Student: Manuel Sascha Weiand
- Date: 03.02.2014
Additional Material
Registration
Registration to the seminar is handled between July 5 and 17, 2013, via the central online form at www.graphics.rwth-aachen.de/apse
Contact
Thomas Noll <noll at cs.rwth-aachen.de>