Skip to main content
  • Conference proceedings
  • © 2017

Verified Software. Theories, Tools, and Experiments

9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 10712)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Conference series link(s): VSTTE: Working Conference on Verified Software: Theories, Tools, and Experiments

Conference proceedings info: VSTTE 2017.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (12 papers)

  1. Front Matter

    Pages I-XIII
  2. A Formally Verified Interpreter for a Shell-Like Programming Language

    • Nicolas Jeannerod, Claude Marché, Ralf Treinen
    Pages 1-18
  3. A Formal Analysis of the Compact Position Reporting Algorithm

    • Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz
    Pages 19-34
  4. Proving JDK’s Dual Pivot Quicksort Correct

    • Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt, Mattias Ulbrich
    Pages 35-48
  5. A Semi-automatic Proof of Strong Connectivity

    • Ran Chen, Jean-Jacques Lévy
    Pages 49-65
  6. Verifying Branch-Free Assembly Code in Why3

    • Marc Schoolderman
    Pages 66-83
  7. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library

    • Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
    Pages 84-101
  8. Automating the Verification of Floating-Point Programs

    • Clément Fumex, Claude Marché, Yannick Moy
    Pages 102-119
  9. 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
  10. Practical Void Safety

    • Alexander Kogtenkov
    Pages 132-151
  11. Memory-Efficient Tactics for Randomized LTL Model Checking

    • Kim Larsen, Doron Peled, Sean Sedwards
    Pages 152-169
  12. An Abstraction Technique for Describing Concurrent Program Behaviour

    • Wytse Oortwijn, Stefan Blom, Dilian Gurov, Marieke Huisman, Marina Zaharieva-Stojanovski
    Pages 191-209
  13. Back Matter

    Pages 211-211

Other Volumes

  1. Verified Software. Theories, Tools, and Experiments

About this book

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.


Editors and Affiliations

  • Paris-Sud University, Orsay, France

    Andrei Paskevich

  • New York University, New York, USA

    Thomas Wies

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access