Verified software : theories, tools, and experiments : 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised selected papers

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. 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