![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
2. VSTTE 2008: Toronto, Canada
- Natarajan Shankar, Jim Woodcock
:
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
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.