Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012 Proceedings

Front Cover
Rajeev Joshi, Peter Müller, Andreas Podelski
Springer Science & Business Media, Jan 10, 2012 - Computers - 326 pages
This volume contains the proceedings of the 4th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2012, held in Philadelphia, PA, USA, in January 2012. The 20 revised full papers presented together with 2 invited talks and 2 tutorials were carefully revised and selected from 54 initial submissions for inclusion in the book. The goal of the VSTTE conference is to advance the state of the art through the interaction of theory development, tool evolution, and experimental validation. The papers address topics such as: specification and verification techniques, tool support for specification languages, tool for various design methodologies, tool integration and plug-ins, automation in formal verification, tool comparisons and benchmark repositories, combination of tools and techniques, customizing tools for particular applications, challenge problems, refinement methodologies, requirements modeling, specification languages, specification/verification case-studies, software design methods, and program logic.
 

What people are saying - Write a review

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

Contents

Cyber War Formal Verification and Certified Infrastructure
1
A Certified Multiprover Verification Condition Generator
2
Integrated Semantics of IntermediateLanguage C and MacroAssembler for Pervasive Formal Verification of Operating Systems and Hypervisors fro...
18
A Basis for Verification of Code Using Pointers
34
Verifying Implementations of Security Protocols by Refinement
50
Deciding Functional Lists with Sublist Sets
66
Developing Verified Programs with Dafny
82
An Exercise in Program Verification
83
Modeling and Validating the Train Fare Calculation and Adjustment SystemUsing VDM++
163
Separation and Sharing
179
An Experience Report
196
Verification of TLB Virtualization Implemented in C
209
A Feasibility Study at BOSCH
225
Our Experience with the CodeContracts Static Checker
241
A Process Specification and Verification Environment
243
Termination Analysis of Imperative Programs Using Bitvector Arithmetic
261

An SMTBased Error Finding Platform
98
A Lightweight Technique for Distributed and Incremental Program Verification
114
Boogie and SireumPilar
130
Bounded Model Checking of C and C++ Programs Using a Compiler IR
146
The Marriage of Exploration and Deduction
162
Specifying and Verifying the Correctness of Dynamic Software Updates
278
Symbolic Execution Enhanced System Testing
294
Infeasible Code Detection
310
Author Index
326
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information