VSTTE '08 Conference Program
by
shankar
—
last modified
2008-08-26 18:34
Schedule for VSTTE'08, Oct 6-9, 2008, Toronto Canada
Date
| Time | Presentation
|
|---|
Oct 6
| 9AM | John Reynolds. Readable Formal Proofs |
| | 10AM | Coffee |
| | 10.30AM | Daniel Leivant. Propositional dynamic logic for recursive procedures |
| | 11AM | Gerwin Klein and Rafal Kolanski. Mapped Separation Logic |
| | 11.30AM | Mark Bickford. Unguessable Atoms: A Logical Foundation for Security |
| | 12noon | Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong. Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems |
| | 12,30PM | Lunch |
| | 2PM | Rick Hehner: Invited Tutorial on Practical Predicative Programming Primer
|
| | 3PM | Patrice Chalin, Perry R. James and George Karabotsos. JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML |
| | 3.30PM | Bruce Weide, Murali Sitaraman, Heather K. Harton, Bruce
Adcock, Paolo Bucci, Derek Bronish, Wayne D. Heym, Jason Kirschenbaum
and David Frazier. Incremental Benchmarks for Software Verification Tools and Techniques |
| | 4PM | Coffee
|
| | 4.30PM | Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone. Verified Protection Model of the seL4 Microkernel |
| | 5PM | Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa and Koichi Takahashi. Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic |
| | 5.30PM | Gregory Dennis, Kuat Yessenov and Daniel Jackson. Bounded Verification of Voting Software |
| | | |
Oct 7
| 9AM | Moshe Vardi. From Verification to Synthesis |
| | 10AM | Coffee |
| | 10.30AM | Joey Coleman. Expression Decomposition in a Rely/Guarantee Context |
| | 11AM | Matthias Daum, Jan Dörrenbächer, Mareike Schmidt and Burkhart Wolff. A Verification Approach for System-level Concurrent Programs |
| | 11.30 | Anindya Banerjee, Michael Barnett and David Naumann. Boogie Meets Regions: a Verification Experience Report |
| | 12noon | Rustan Leino, Peter Müller and Angela Wallenburg. Flexible Immutability with Frozen Objects |
| | 12,30PM | Lunch |
| | 2PM | Leonardo de Moura: Invited Tutorial on SMT@Microsoft
|
| | 3PM | Short Presentations
|
| | 4PM | Coffee |
| | 4.30PM | Eyad Alkassar, Mark Hillebrand, Dirk Leinenbach, Norbert W. Schirmer and Artem Starostin. The Verisoft Approach to Systems Verification |
| | 5PM
| | Eyad Alkassar and Mark Hillebrand. Formal Functional Verification of Device Drivers |
|
| | 5.30PM | | Artem Starostin and Alexandra Tsyban. Verified Process-Context Switch for C-Programmed Kernels |
|
| | | |
Oct 8
| 9AM | Sriram Rajamani. Combining Tests and Proofs |
| | 10AM | Coffee |
| | 10.30AM | Ernie Cohen: Invited Tutorial on Verifying the Microsoft Hypervisor
|
| | 11.30AM | Panel on Making Verification Mainstream
|
| | 12.30PM | Lunch |
| | 2PM | Walking Tour of Toronto
|
| | 6PM | Cruise + Banquet
|
Oct 9
| 9AM | Andreas Podelski. Verification, Least-Fixpoint Checking, Abstraction |
| | 10.30AM | Workshops on Theory, Tools, and Experiments
|