Programme
| Monday, 25.02.2008 | ||
| 09:15 | Ralf Huuck, Gerwin Klein, and Bastian Schlich | Welcome |
| 09:30 | Invited Talk by Kim Larsen |
Validation, Performance Analysis and Synthesis of Embedded Systems |
| 10:30 | Morning Tea | |
| 11:00 | Par Emanuelsson and Ulf Nilsson | A Comparative Study of Industrial Static Analysis Tools |
| 11:45 | Dirk Leinenbach and Elena Petrova | Pervasive Compiler Verification - From Verified Programs to Verified Systems |
| 12:30 | Lunch | |
| 13:30 | Harvey Tuch | Structured Types and Separation Logic |
| 14:15 | Rafal Kolanski | A Logic for Virtual Memory |
| 15:00 | Afternoon Tea | |
| 15:45 | Hendrik Tews, Tjark Weber and Marcus Völp | A Formal Model of Memory Peculiarities for the
Verification of Low-Level Operating-System Code |
| 16:30 | Christof Efkemann and Tobias Hartmann | Specification of Conditions for Error Diagnostics |
| 17:15 | End |
| Tuesday, 26.02.2008 | ||
| 09:30 | Invited Talk by Hongseok Yang | On Scalable Shape Analysis |
| 10:30 | Morning Tea | |
| 11:00 | Jan Peleska and Loeding Helge | Symbolic and Abstract Interpretation for C/C++ Programs |
| 11:45 | Gerlind Herberich, Bastian Schlich, Weise Carsten and Thomas Noll | Proving Correctness of an Efficient Abstraction for Interrupt Handling |
| 12:30 | Lunch | |
| 13:30 | Tom In der Rieden and Alexandra Tsyban | CVM - A Verified Framework for Microkernel Programmers |
| 14:15 | Artem Starostin and Alexandra Tsyban | Correct Microkernel Primitives |
| 15:00 | Afternoon Tea | |
| 15:45 | Paul Graunke | Verified Safety and Information Flow of a Block Device |
| 16:30 | End | |
| 18:30 | Social Event |
| Wednesday, 27.02.2008 | ||
| 9:30 | Kirsten Berkenkötter | Reliable UML Models and Profiles |
| 10:15 | Tony Cant, Ben Long, Jim McCarthy, Brendan Mahony and Kylie Williams | The HiVe Writer |
| 11:00 | Morning Tea | |
| 11:30 | Christof Efkemann, Helge Löding and Jan Peleska | Test Automation and Static Analysis with RT-Tester |
| 12:15 | Ansgar Fehnker | PRISM for Wireless Networks |
| 13:00 | Lunch | |
| 14:00 | Bastian Schlich | [mc]square - A Model Checker for Microcontroller Assembly Code |
| 14:45 | Ralf Huuck | Goanna |
| 15:30 | Wrap up |
|
| 16:00 | End |