The goals of this course are:
Note that students are expected to attend all sessions.
Lectures are held in room 0.1.12 on mondays from 12:30 to 14:15.
| # | Date | Topic (speaker(s)) |
|---|---|---|
| 1 | 08 SEP | Course introduction (HH) [slides] |
| Assigning papers to be presented | ||
| 2 | 15 SEP |
Typing
One-to-One and One-to-Many Correspondences in Security Protocols By Andrew D. Gordon and Alan Jeffrey
Presenter: Palle Raabjerg
Opponent: Jesper Brix Rosenkilde |
|
Automatically
Validating Temporal Safety Properties of Interfaces
By Thomas Ball and Sriram K. Rajamani
Presenter: Mads Christian Olesen
Opponent: Martin Toft |
||
| 3 | 22 SEP |
Bisimulation through Probabilistic Testing By Kim Guldstrand Larsen and Arne Skou
Presenter: Jan Kretinsky
Opponent: Kenneth Blanner Holleufer |
|
Modelling
and Verification of the LMAC Protocol for Wireless Sensor Networks
By A Fehnker, A Mader, and L van Hoesel
Presenter: M. Saleem Vighio
Opponent: Andreas Engelbredt Dalsgaard |
||
| 4 | 29 SEP |
Specification
and Refinement of Probabilistic Processes By Bengt Jonsson and Kim Guldstrand Larsen
Presenter: Nikola Benes
Opponent: Jesper Brix Rosenkilde |
|
CTL Model Checking
By Baier and Katoen
Presenter: Martin Toft
Opponent: Palle Raabjerg |
||
| 5 | 06 OKT |
Planning as model checking for extended
goals in non-deterministic domains By M. Pistore and P. Traverso
Presenter: Kenneth Blanner Holleufer
Opponent: Jan Kretinsky |
|
Applying
Compiler Techniques to Cache Behavior Prediction
By Christian Ferdinand, Florian Martin, and Reinhard Wilhelm
Presenter: Andreas Engelbredt Dalsgaard
Opponent: Mads Christian Olesen |
||
| 6 | 20 OKT |
Symbolic controller synthesis for discrete and timed
systems
By Eugene Asarin, Oded Maler, and Amir Pnueli
Presenter: Jesper Brix Rosenkilde
Opponent: M. Saleem Vighio |
|
A Type Discipline for Authorization Policies
By Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis
Presenter: Palle Raabjerg
Opponent: Nikola Benes |
||
| 7 | 27 OKT |
Model-based
Schedulability Analysis of Safety Critical Hard Real-Time Java
Programs By Thomas Bøgholm, Henrik Kragh-Hansen, Petur Olsen, Bent Thomsen, and Kim G. Larsen
Presenter: Mads Christian Olesen
Opponent: Kenneth Blanner Holleufer |
|
Improved
Upper and Lower Bounds for Modal Logics of Programs
By Moshe Y. Vardi and Larry J. Stockmeyer
Presenter: Jan Kretinsky
Opponent: Andreas Engelbredt Dalsgaard |
||
| 8 | 03 NOV |
Formal
Verification and Simulation for Performance Analysis for
Probabilistic Broadcast Protocols
By Ansgar Fehnker and Peng Gao
Presenter: M. Saleem Vighio
Opponent: N/A |
|
Interface
Input/Output Automata
By Kim G. Larsen, Ulrik Nyman, and Andrzej Wasowski
Presenter: Nikola Benes
Opponent: N/A |
||
| 9 | 10 NOV |
Sensitivity Analysis of Cache Replacement Policies
By Jan Reineke og Daniel Grund
Presenter: Martin Toft
Opponent: Jan Kretinsky |
|
Strategic Planning through Model Checking of ATL Formulae
By Wojciech Jamroga
Presenter: Kenneth Blanner Holleufer
Opponent: Palle Raabjerg |
||
| 10 | 17 NOV |
The
Influence of Processor Architecture on the Design and
the Results of WCET Tools
By Heckmann, R.; Langenbach, M.; Thesing, S.; Wilhelm, R.
Presenter: Andreas Engelbredt Dalsgaard
Opponent: Nikola Benes |
|
Efficient on-the-fly algorithms for the analysis of timed games
By Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, Didier Lime
Presenter: Jesper Brix Rosenkilde
Opponent: M. Saleem Vighio |
||
| 11 | 24 NOV |
Type-Based Verification of Correspondence Assertions
for Communication Protocols
By Daisuke Kikuchi and Naoki Kobayashi
Presenter: Palle Raabjerg
|
|
Why Model Checking Can Improve WCET Analysis
By Alexander Metzner
Presenter: Mads Christian Olesen
|
||
|
Probabilistic Propositional Temporal Logics
By Sergiu Hart and Micha Sharir
Presenter: Jan Kretinsky
|
||
| 12 | 01 DEC |
Does Clock Precision Influence ZigBee's Energy Consumptions?
By Christian Groß, Holger Hermanns, Reza Pulungan
Presenter: Saleem M. Vighio
|
|
TBA
By TBA
Presenter: Nikola Benes
|
||
|
Automatic Identification of Timing Anomalies for Cycle-Accurate
Worst-Case Execution Time Analysis
By J. Eisinger, I. Polian, B. Becker, A. Metzner, S. Thesing og R. Wilhelm.
Presenter: Martin Toft
|
||
| 13 | 08 DEC |
TBA
By TBA
Presenter: Kenneth Blanner Holleufer
|
|
TBA
By TBA
Presenter: Andreas Engelbredt Dalsgaard
|
||
|
TBA
By TBA
Presenter: Jesper Brix Rosenkilde
|