Skip to main content



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
Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.