Tentative Programme
| Saturday, August 26: | |
| 9:00 - 10:00 | Invited Talk |
| Challenges for Formal Verification in Industrial Setting
Anna Slobodova |
|
| 10:00 - 10:30 | An easy-to-use, efficient tool-chain to analyze the availability of telecommunication equipment
M. Siegle, K. Lampka, M. Walter |
| 10:30 - 11:00 | Coffee Break |
| 11:00 - 12:30 | Handling large state spaces |
| "To Store or Not To Store" Reloaded: Reclaiming Memory on Demand
M. Weber, M. Hammer |
|
| Discovering Symmetries
H. Saidi |
|
| On Combining Partial Order Reduction with Fairness Assumptions
L. Brim, I. Cerna, P. Moravec, J. Simsa |
|
| 12:30 - 14:30 | Lunch Break |
| 14:30 - 16:00 | Model based testing |
| Test Coverage for Loose Timing Annotations
F. Maraninchi, C. Helmstetter, L. Maillet-Contoz |
|
| Model Based Testing of a WAP Gateway
A. Hessel, P. Pettersson |
|
| Heuristics for ioco-Based Test-Based Modelling
T. Willemse |
|
| 16:00 - 16:30 | Coffee Break |
| 16:30 - 18:00 | Case studies I |
| Verifying VHDL Designs with Multiple Clocks in SMV
A. Smrcka, P. Matousek, Z. Rehak, D. Safranek, T. Vojnar, V. Rehak |
|
| Verified Design of an Automated Parking Garage
A. Mathijssen, A. J. Pretorius |
|
| Evaluating quality of service for service level agreements
S. Gilmore, A. Clark |
|
| 19:30 - 22:30 | Conference Dinner |
| Sunday, August 27: | |
| 9:30 - 10:30 | Invited Talk, Joint with CONCUR |
| Making Concurrency Mainstream
Edward Lee |
|
| 10:30 - 11:00 | Coffee Break |
| 11:00 - 12:30 | Case studies II |
| Simulation-based Performance Analysis of a Medical Image-Processing Architecture
P. Cuijpers, A. Fyukov |
|
| BLASTing Linux Code
J. T. Muehlberg, G. Luettgen |
|
| A Finite State Modelling of AFDX Frame Management using SPIN
S. Roy, I. Sahal |
|
| 12:30 - 14:30 | Lunch Break |
| 14:30 - 16:00 | Formal description and analyzis techniques |
| UML 2.0 State Machines: Complete Formal Semantics via Core State Machines
H. Fecher, J. Schoenborn |
|
| Automated Incremental Synthesis of Timed Automata
B. Bonakdarpour, S. S. Kulkarni |
|
| SAT-based Verification of LTL formulas
W. Zhang |
|
| 16:00 - 16:30 | Coffee Break |
| 16:30 - 18:00 | Tools session |
| jmle: A Tool for Executing JML Specifications via Constraint Programming
T. Wahls, B. Krause |
|
| Goanna - A Static Model Checker
R. Huuck, A. Fehnker, F. Rauch, M. Lussenburg, P. Jayet |
|
| jETI repository of verification tools
T. Margaria |
|
| 18:00 - 19:00 | FMICS bussiness meeting |