Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers

✍ Scribed by Dimitra Giannakopoulou, Daniel Kroening (eds.)

• Publisher: Springer International Publishing
• Year: 2014
• Tongue: English
• Leaves: 291
• Series: Lecture Notes in Computer Science 8471 Programming and Software Engineering
• Edition: 1
• Category: Library

✦ Synopsis

This volume constitutes the thoroughly refereed post-conference proceedings of the 6th International Conference on Verified Software: Theories, Tools and Experiments, VSTTE 2014, held in July 2014 at the Vienna Summer of Logic in Vienna, Austria, as an associated event of CAV 2014, the International Conference on Computer-Aided Verification. The 17 revised full papers presented were carefully revised and selected from 34 submissions. The papers are organized in topical sections such as analysis: understanding and explanation; verification frameworks and applications; hypervisors and dynamic data structures; certification; real time and security.

✦ Table of Contents

Front Matter....Pages I-X
Front Matter....Pages 1-1
A Logical Analysis of Framing for Specifications with Pure Method Calls....Pages 3-20
Efficient Refinement Checking in VCC....Pages 21-36
Formalizing Semantics with an Automatic Program Verifier....Pages 37-51
Front Matter....Pages 53-53
The KeY Platform for Verification and Analysis of Java Programs....Pages 55-71
A Verification Condition Visualizer....Pages 72-86
Formal Modeling and Verification of CloudProxy....Pages 87-104
Using Promela in a Fully Verified Executable LTL Model Checker....Pages 105-114
Front Matter....Pages 115-115
Store Buffer Reduction with MMUs....Pages 117-132
Separation Kernel Verification: The Xtratum Case Study....Pages 133-149
Separation Algebras for C Verification in Coq....Pages 150-166
Automatically Verified Implementation of Data Structures Based on AVL Trees....Pages 167-180
Front Matter....Pages 181-181
A Model for Capturing and Replaying Proof Strategies....Pages 183-199
A Certifying Frontend for (Sub)polyhedral Abstract Domains....Pages 200-215
Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations....Pages 216-232
Front Matter....Pages 233-233
Parameterized Model-Checking of Timed Systems with Conjunctive Guards....Pages 235-251
Timed Refinement for Verification of Real-Time Object Code Programs....Pages 252-269
What Gives? A Hybrid Algorithm for Error Trace Explanation....Pages 270-286
Back Matter....Pages 287-287

✦ Subjects

Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Programming Techniques; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics)