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

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.

---

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.

---

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.

Content:
Front Matter....Pages -
Cyber War, Formal Verification and Certified Infrastructure....Pages 1-1
A Certified Multi-prover Verification Condition Generator....Pages 2-17
Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT....Pages 18-33
The Location Linking Concept: A Basis for Verification of Code Using Pointers....Pages 34-49
Verifying Implementations of Security Protocols by Refinement....Pages 50-65
Deciding Functional Lists with Sublist Sets....Pages 66-81
Developing Verified Programs with Dafny....Pages 82-82
Verifying Two Lines of C with Why3: An Exercise in Program Verification....Pages 83-97
Development and Evaluation of LAV: An SMT-Based Error Finding Platform....Pages 98-113
A Lightweight Technique for Distributed and Incremental Program Verification....Pages 114-129
A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar....Pages 130-145
The Marriage of Exploration and Deduction....Pages 146-161
Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++....Pages 162-162
Formalized Verification of Snapshotable Trees: Separation and Sharing....Pages 163-178
Comparing Verification Condition Generation with Symbolic Execution: An Experience Report....Pages 179-195
Verification of TLB Virtualization Implemented in C....Pages 196-208
Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH....Pages 209-224
Our Experience with the CodeContracts Static Checker....Pages 225-240
Isabelle/Circus: A Process Specification and Verification Environment....Pages 241-242
Termination Analysis of Imperative Programs Using Bitvector Arithmetic....Pages 243-260
Specifying and Verifying the Correctness of Dynamic Software Updates....Pages 261-277
Symbolic Execution Enhanced System Testing....Pages 278-293
Infeasible Code Detection....Pages 294-309
Back Matter....Pages 310-325
....Pages -