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 BibTeX

Keynote Talks (Abstracts)

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

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

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

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

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

Colin O'Halloran:
Where Is the Value in a Program Verifier?. 255-262
Electronic Edition (link) BibTeX