2. VSTTE 2008: Toronto, Canada

Natarajan Shankar, Jim Woodcock (Eds.): Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings . Lecture Notes in Computer Science 5295 Springer 2008, ISBN 978-3-540-87872-8

Keynote Talks (Abstracts)

John C. Reynolds:
Readable Formal Proofs. 1
Moshe Y. Vardi:
From Verification to Synthesis. 2
Andreas Podelski:
Verification, Least-Fixpoint Checking, Abstraction. 3
Madhu Gopinathan, Aditya V. Nori, Sriram K. Rajamani:
Combining Tests and Proofs. 4-5

Logics

Daniel Leivant:
Propositional Dynamic Logic for Recursive Procedures. 6-14
Rafal Kolanski, Gerwin Klein:
Mapped Separation Logic. 15-29
Mark Bickford:
Unguessable Atoms: A Logical Foundation for Security. 30-53
Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong:
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. 54-69

Tools

Patrice Chalin, Perry R. James, George Karabotsos:
JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML. 70-83
Bruce W. Weide, Murali Sitaraman, Heather K. Harton, Bruce M. Adcock, Paolo Bucci, Derek Bronish, Wayne D. Heym, Jason Kirschenbaum, David Frazier:
Incremental Benchmarks for Software Verification Tools and Techniques. 84-98

Case Studies

Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone:
Verified Protection Model of the seL4 Microkernel. 99-114
Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, Koichi Takahashi:
Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic. 115-129
Greg Dennis, Kuat Yessenov, Daniel Jackson:
Bounded Verification of Voting Software. 130-145

Methodology

Joey W. Coleman:
Expression Decomposition in a Rely/Guarantee Context. 146-160
Matthias Daum, Jan Dörrenbächer, Mareike Schmidt, Burkhart Wolff:
A Verification Approach for System-Level Concurrent Programs. 161-176
Anindya Banerjee, Michael Barnett, David A. Naumann:
Boogie Meets Regions: A Verification Experience Report. 177-191
K. Rustan M. Leino, Peter Müller, Angela Wallenburg:
Flexible Immutability with Frozen Objects. 192-208

Verisoft

Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert Schirmer, Artem Starostin:
The Verisoft Approach to Systems Verification. 209-224
Eyad Alkassar, Mark A. Hillebrand:
Formal Functional Verification of Device Drivers. 225-239
Artem Starostin, Alexandra Tsyban:
Verified Process-Context Switch for C-Programmed Kernels. 240-254

Paper from VSTTE 2005

Colin O'Halloran:
Where Is the Value in a Program Verifier?. 255-262