Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers

✍ Scribed by Andrei Paskevich,Thomas Wies (eds.)

• Publisher: Springer International Publishing
• Year: 2017
• Tongue: English
• Leaves: 223
• Series: Programming and Software Engineering 10712
• Edition: 1
• Category: Library

✦ Synopsis

This volume constitutes the thoroughly refereed post-conference proceedings of the 9th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, held in Heidelberg, Germany, in July 2017.
The 12 full papers presented were carefully revised and selected from 20 submissions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies.

✦ Table of Contents

Front Matter ....Pages I-XIII
A Formally Verified Interpreter for a Shell-Like Programming Language (Nicolas Jeannerod, Claude Marché, Ralf Treinen)....Pages 1-18
A Formal Analysis of the Compact Position Reporting Algorithm (Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz)....Pages 19-34
Proving JDK’s Dual Pivot Quicksort Correct (Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt, Mattias Ulbrich)....Pages 35-48
A Semi-automatic Proof of Strong Connectivity (Ran Chen, Jean-Jacques Lévy)....Pages 49-65
Verifying Branch-Free Assembly Code in Why3 (Marc Schoolderman)....Pages 66-83
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library (Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond)....Pages 84-101
Automating the Verification of Floating-Point Programs (Clément Fumex, Claude Marché, Yannick Moy)....Pages 102-119
Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions (Saeed Nejati, Jia Hui Liang, Catherine Gebotys, Krzysztof Czarnecki, Vijay Ganesh)....Pages 120-131
Practical Void Safety (Alexander Kogtenkov)....Pages 132-151
Memory-Efficient Tactics for Randomized LTL Model Checking (Kim Larsen, Doron Peled, Sean Sedwards)....Pages 152-169
Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency Models (Tatsuya Abe, Tomoharu Ugawa, Toshiyuki Maeda)....Pages 170-190
An Abstraction Technique for Describing Concurrent Program Behaviour (Wytse Oortwijn, Stefan Blom, Dilian Gurov, Marieke Huisman, Marina Zaharieva-Stojanovski)....Pages 191-209
Back Matter ....Pages 211-211

✦ Subjects

Software Engineering