Verified Software: Theories, Tools, Experiments: Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008, Proceedings

Front Cover
Natarajan Shankar, James Woodcock
Springer Science & Business Media, Sep 22, 2008 - Computers - 263 pages

This volume contains the proceedings of the second working conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2008, held in Toronto, Canada, in October 2008.

The 16 papers presented together with 4 invited talks were carefully revised and selected for inclusion in the book. This second conference formally inaugurates the Verified Software Initiative (VSI), a fifteen-year, co-operative, international project directed at the scientific challenges of large-scale software verification. The scope of the cooperative effort includes the sharing and interoperability of tools, the alignment of theory and practice, the identification of challenge problems, the construction of benchmark suites, and the execution of large-scale experiments.

 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Readable Formal Proofs
1
From Verification to Synthesis
2
Verification LeastFixpoint Checking Abstraction
3
Combining Tests and Proofs
4
Propositional Dynamic Logic for Recursive Procedures
6
Mapped Separation Logic
15
A Logical Foundation for Security
30
Combining DomainSpecific and Foundational Logics to Verify Complete Software Systems
54
Bounded Verification of Voting Software
130
Expression Decomposition in a RelyGuarantee Context
146
A Verification Approach for SystemLevel Concurrent Programs
161
A Verification Experience Report
177
Flexible Immutability with Frozen Objects
192
The Verisoft Approach to Systems Verification
209
Formal Functional Verification of Device Drivers
225
Verified ProcessContext Switch for CProgrammed Kernels
240

Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML
70
Incremental Benchmarks for Software Verification Tools and Techniques
84
Verified Protection Model of the seL4 Microkernel
99
Verification of the DeutschSchorrWaite Marking Algorithm with Modal Logic
115
Where Is the Value in a Program Verifier?
255
Author Index
263
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information