Workshop Program
Invited talks and tutorial abstracts
| June 26 (Friday) |
Day 1 | |
|---|---|---|
| 8:45 — 9:00 | Welcome |
|
| 9:00 — 10:00 | Invited
Talk Amir
Pnueli, (Computer Science Department, Courant Institute of mathematical Sciences, New York University) |
|
| 10:00 — 10:30 | Break I | |
| 10:30 — 12:30 | Tutorial 1 Grigore Rosu (UIUC) Runtime Verification using MOP |
|
| 12:30 — 2:00 | Lunch | |
| 2:00 — 3:30 | Session
1: SPECIFICATION LANGUAGES Chair: Klaus Havelund |
|
| 2:00 — 2:30 |
Isabel Nunes, Antonia
Lopes and Vasco Vasconcelos Bridging the Gap Between Algebraic Specification and Object-Oriented Generic Programming |
|
| 2:30 — 3:00 | Kari
Kahkonen, Jani Lampinen, Keijo
Heljanko and Ilkka Niemel The LIME Interface Specification Language and Runtime Monitoring Tool (TOOL paper) |
|
| 3:00 — 3:30 | Ylies Falcone, Jean-Claude
Fernandez and Laurent Mounier Runtime Verification of Safety-Progress Properties |
|
| 3:30 — 4:00 | Break II | |
| 4:00 — 5:00 | Session
2: MONITORS AS HARDWARE Chair: Grigore Rosu |
|
| 4:00 — 4:30 | Antonia Zhai, Guojin
He and Mats Heimdahl Hardware and compiler support for dynamic software monitoring |
|
| 4:30 — 5:00 | Bernd Finkbeiner and
Lars Kuhtz Monitor Circuits for LTL with Bounded and Unbounded Future |
|
| June 27 (Saturday) |
Day 2 | |
|---|---|---|
| 9:00 — 10:00 | Invited
Talk Sriram Rajamani (Microsoft Research India) |
|
| 10:00 — 10:30 | Break I | |
| 10:30 — 12:30 | Tutorial
2 Nikolai Tillmann, Microsoft Research Parameterized Unit Testing with Pex, a White Box Test Input Generation Tool for .NET |
|
| 12:30 — 2:00 | Lunch | |
| 2:00 — 3:30 | Session
3: CONCURRENCY AND MEMORY MANAGEMENT Chair: Oleg Sokolsky |
|
| 2:00 — 2:30 |
Yarden Nir-Buchbinder,
Zdenek Letko, Bohuslav Krena, Rachel Tzoref-Brill, Shmuel Ur and Tomas
Vojnar A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing (TOOL paper) |
|
| 2:30 — 3:00 | Grigore Rosu, Wolfram
Schulte and Traian Serbanuta Runtime Verification of C Memory Safety |
|
| 3:00 — 3:30 | Philipp Adler and Amme
Wolfram Type-Separated Bytecode -- Its Construction and Evaluation |
|
| 3:30 — 4:00 | Break II | |
| 4:00 — 5:30 | Session
4: DIAGNOSIS AND DISTRIBUTED SYSTEMS Chair: Howard Barringer |
|
| 4:00 — 4:30 | Stavros Tripakis A Combined On-line/Off-line Framework for Black-Box Fault Diagnosis |
|
| 4:30 — 5:00 | Trevor Hansen, Peter
Schachte and Harald Sondergaard State Joining and Splitting for the Symbolic Execution of Binaries |
|
| 5:00 — 5:30 | Wenchao Zhou, Oleg
Sokolsky, Boon Thau Loo and Insup Lee DMaC: Distributed Monitoring and Checking |
|
| June 28 (Sunday) |
Day 3 | |
|---|---|---|
| 9:00 — 10:00 | Tutorial 3 Howard Barringer (Manchester University) Rule-based Systems for Run-time Verification and Log File Analysis |
|
| 10:00 — 10:30 | Break I | |
| 10:30 — 11:30 | Tutorial 3 (continued) Klaus Havelund (JPL, Nasa) Rule-based Systems for Run-time Verification and Log File Analysis |
|
| 11:30 — 12:30 | Business Meeting | |