Programme
Day 1: Monday 24 August
| 11:00 | Registration |
| 12:30 | Lunch |
| 14:00 | Tutorial session 1 Michael Tautschnig CBMC: Bounded Model Checking of Concurrent C Programs |
| 15:30 | Break |
| 16:00 | Tutorial session 2 (CBMC continued) |
| 17:30 | Close |
| 19:00 | Opening reception at De Warenmarkt (c/o Plein and Ryneveld) |
Day 2: Tuesday 25 August
| 8:00 | Registration & coffee |
| 9:15 | Welcoming |
| 9:30 | Invited Talk 1 Tevfik Bultan String Analysis for Vulnerability Detection and Repair |
| 10:30 | Break |
| 11:00 | Session 1: Abstraction, Refinement, Translation (A Fillieri) Backes, Reineke: ASTRA: A tool for abstract interpretation of graph transformation systems Beyer, Löwe, Wendler: Refinement Selection Klarl: From Helena Ensemble Specifications to Promela Verification Models |
| 12:30 | Lunch |
| 14:00 | Session 2: Büchi Automata & Hashing (M Frias) Barnat, Rockai, Štill, Weiser: Fast, Dynamically-Sized Concurrent Hash Table Blahoudek, Duret-Lutz, Rujbr, Strejček: On Refinement of Büchi Automata for Explicit Model Checking Michaud, Duret-Lutz: Practical Stutter-Invariance Checks for ω-Regular Languages |
| 15:30 | Break |
| 16:00 | Session 3: Embedded Systems (W Visser) Chattopadhyay: MESS: Memory Performance Debugging on Embedded Multi-core Systems Ismail, Bessa, Cordeiro, Lima Filho, Chaves Filho: DSVerifier: A Bounded Model Checking Tool for Digital Systems Espada, Salmerón, Gallardo, Merino: Runtime verification of expected Energy Consumption in Smartphone |
| 17:30 | Close |
| 19:00 | Banquet at Tokara Bus leaves from City Hall (c/o Plein and Andringa) at 18:45 |
Day 3: Wednesday 26 August
| 9:00 | Coffee |
| 9:30 | Invited Talk 2 Willem Visser The Augmented Reality of Model Counting |
| 10:30 | Break |
| 11:00 | Session 4: Heuristics & Benchmarks (L Cordeiro) Andisha, Wehrle, Westphal: Directed Model Checking for PROMELA with Relaxation-Based Distance Functions Beyer, Löwe, Wendler: Benchmarking and Resource Measurement – Application to Automatic Verification Sorrentino: PickLock: A Deadlock Prediction Approach under Nested Locking |
| 12:30 | Lunch |
| 14:00 | Session 5: SAT/SMT-Based Approaches (P Merino) Beer, Heidinger, Kühne, Leitner-Fischer, Leue: Symbolic Causality Checking using Bounded Model Checking Filieri, Frias, Pasareanu, Visser: Model Counting for Complex Data Structures Timm, Gruner, Sibanda: Parallel SAT-Based Parameterised Three-Valued Model Checking |
| 15:30 | Break |
| 16:00 | Session 6: Software Validation & Verification (J Strejček) Biondi, Legay, Quilbeuf: Comparative Analysis of Leakage Tools on Scalable Case Studies Dimovski, Al-Sibahi, Brabrand, Wasowski: Family-Based Model Checking without a Family-Based Model Checker Christakis, Godefroid: IC-Cut: A Compositional Search Strategy for Dynamic Test Generation |
| 17:30 | Close |
| 19:00 | Dinner at Oppie Dorp (137 Dorp Street) |
Day 4: Thursday 27 August
| 8:45-19 | Conference excursion We leave 8:45 from the Town Hall (c/o Plein and Andringa). If you have to leave early to be at the airport, we suggest a metered taxi after lunch; the cost will be roughly R400. |
