|
WORKSHOP SESSIONS
Session papers with links below are available to workshop registrants immediately and to everyone beginning October 6, 2010.
All sessions will take place in the Boardroom unless otherwise noted.
|
Wednesday, October 6, 2010
|
| 3:00 p.m.–3:05 p.m.
|
|
Welcome
Program Co-Chairs: Gerwin Klein, Ralf Huuck, and Bastian Schlich
|
| 3:05 p.m.–4:00 p.m. |
|
Invited Talk
Static Analysis for Verifying C Programs, and More
Pascal Cuoq, CEA
|
| 4:00 p.m.–4:30 p.m. Break
|
 |
| 4:30 p.m.–5:30 p.m. |
|
Typed Assembly Language for Implementing OS Kernels in SMP/Multi-Core Environments with Interrupts
Toshiyuki Maeda and Akinori Yonezawa, University of Tokyo
Read the Abstract | Full paper | Slides
Counterexample-Guided Abstraction Refinement for PLCs
Sebastian Biallas, Jörg Brauer, and Stefan Kowalewski, Embedded Software Laboratory, RWTH Aachen University
Read the Abstract | Full paper | Slides
|
| 6:30 p.m. Workshop Dinner, Vancouver Island Room
|
|
Thursday, October 7, 2010
|
| 8:00 a.m.–9:00 a.m. Continental Breakfast, Vancouver Island Room
|
|
| 9:00 a.m.–10:30 a.m.
|
|
Invited Talk
Visualizing Information Flow through C Programs
Joe Hurd, Galois Inc.
Refereed Paper
dBug: Systematic Evaluation of Distributed Systems
Jiri Simsa, Randy Bryant, and Garth Gibson, Carnegie Mellon University
Read the Abstract | Full paper | Slides
|
| 10:30 a.m.–11:00 a.m. Break
|
|
| 11:00 a.m.–12:30 p.m. |
|
Model-based Testing Without a Model: Assessing Portability in the Seattle Testbed
Justin Cappos and Jonathan Jacky, University of Washington
Read the Abstract | Full paper | Slides
Correctness Proofs for Device Drivers in Embedded Systems
Jianjun Duan and John Regehr, University of Utah
Read the Abstract | Full paper | Slides
Lyrebird—Assigning Meanings to Machines
David Cock, NICTA and University of New South Wales
Read the Abstract | Full paper | Slides
|
| 12:30 p.m.–1:30 p.m. Workshop Luncheon, Vancouver Island Room
|
|
| 1:30 p.m.–3:00 p.m. |
|
Invited Talk
Work in Progress for the Next 100Mloc: Finding Bugs in Real Code
Ansgar Fehnker, NICTA and University of New South Wales
Refereed Paper
A Precise Memory Model for Low-Level Bounded Model Checking
Carsten Sinz, Stephan Falke, and Florian Merz, Institute for Theoretical Computer Science, Karlsruhe Institute of Technology
Read the Abstract | Full paper | Slides
|
| 3:00 p.m.–3:30 p.m. Break
|
|
| 3:30 p.m.–4:30 p.m. |
|
Verification of Stack Manipulation in the SCIP Processor
J. Aaron Pendergrass, Johns Hopkins University Applied Physics Laboratory
Read the Abstract | Full paper | Slides
Towards Proving Security in the Presence of Large Untrusted Components
June Andronick, NICTA and University of New South Wales; David Greenaway, NICTA; Kevin Elphinstone, NICTA and University of New South Wales
Read the Abstract | Full paper | Slides
|
| 4:30 p.m.–5:00 p.m. Break
|
|
| 5:00 p.m.–5:30 p.m.
|
|
Loop Refinement Using Octagons and Satisfiability
Jörg Brauer, Volker Kamin, and Stefan Kowalewski, Embedded Software Laboratory, RWTH Aachen University; Thomas Noll, Software Modelling and Verification Group, RWTH Aachen University
Read the Abstract | Full paper
|
Need help?
Use our Contacts page.
