VSTTE 2017

9th Working Conference on Verified Software: Theories, Tools, and Experiments

July 22-23, 2017, Heidelberg, Germany
Co-located with the 29th International Conference on Computer-Aided Verification (CAV 2017)



Submissions | Important Dates | Organization | Program | Invited Speakers | Program Chairs | Program Committee

Overview

The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation.

We welcome submissions describing significant advances in the production of verified software, i.e., software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies.

Topics of interest for this conference include education, requirements modeling, specification languages, specification/verification/certification case studies, formal calculi, software design methods, automatic code generation, refinement methodologies, compositional analysis, verification tools (e.g., static analysis, dynamic analysis, model checking, theorem proving, satisfiability), tool integration, benchmarks, challenge problems, and integrated verification environments.

Paper Submissions

We accept both long (limited to 16 pages, references not included) and short (limited to 10 pages, references not included) paper submissions. Short submissions also cover Verification Pearls describing an elegant proof or proof technique. Submitted research papers and system descriptions must be original and not submitted for publication elsewhere. Each submission will be evaluated by at least three members of the Program Committee. We expect that one author of every accepted paper will present their work at the conference.

Research paper submissions must be written in English using the LNCS LaTeX format and must include a cogent and self-contained description of the ideas, methods, results, and comparison to existing work.

Papers will be submitted via EasyChair at the VSTTE 2017 conference page. The post-conference proceedings of VSTTE 2017 will be published in the LNCS series. Authors of accepted papers will be requested to sign the copyright transfer form. A selection of best papers will be invited for publication in the Journal of Automated Reasoning.

Important Dates

Organization

Registration to VSTTE is part of the CAV registration process. If you want to register only for workshops, proceed as follows:

  1. Log in to the registration site and start registration.
  2. On the first page, when it shows the different options for conference registration, do not select any option but just click the “Next step” button at the bottom of the page.
  3. This will take you to the workshop registration page and you can select one of the options.

VSTTE will take place at the Crowne Plaza hotel, Kurfürsten-Anlage 1, Heidelberg.

[preliminary] Program

Saturday, July 22

9:00-10:00 Invited speaker: Santiago Zanella-Beguelin
TBA
Session 1 SAT solving for cryptographic analysis
10:00-10:30 Saeed Nejati, Jia Liang, Catherine Gebotys, Krzysztof Czarnecki, and Vijay Ganesh
Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions
10:30-11:00 coffee break
Session 2 Program verification — Case studies
11:00-11:30 Aaron Dutle, Mariano Moscato, Laura Titolo, and Cesar Munoz
A Formal Analysis of the Compact Position Reporting Algorithm
11:30-12:00 Bernhard Beckert, Jonas Schiffl, Peter Schmitt, and Mattias Ulbrich
Proving JDK's Dual Pivot Quicksort Correct
12:00-12:30 Ran Chen and Jean-Jacques Levy
A Semi-Automatic Proof of Strong Connectivity
12:30-14:00 lunch break
14:00-15:00 Invited speaker: Christoph Weidenbach
Design Principles of Automated Reasoning Systems
Session 3 Numeric computations I
15:00-15:30 Marc Schoolderman
Verifying Branch-Free Assembly Code Using Why3
15:30-16:00 coffee break
Session 4 Numeric computations II
16:00-16:30 Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
16:30-17:00 Clément Fumex, Claude Marché, and Yannick Moy
Automating the Verification of Floating-Point Programs

Sunday, July 23

9:00-10:00 Invited speaker: Jan Hoffman
Why Verification Cannot Ignore Resource Usage
Session 5 Intermediate verification languages
10:00-10:30 Nicolas Jeannerod, Ralf Treinen, and Claude Marché
A Formally Verified Interpreter for a Shell-like Programming Language
10:30-11:00 coffee break
Session 6 Static analysis and model checking
11:00-11:30 Alexander Kogtenkov
Practical Void Safety
11:30-12:00 Kim Guldstrand Larsen, Doron Peled, and Sean Sedwards
Memory-Efficient Tactics for Randomized LTL Model Checking
12:00-12:30 Tatsuya Abe, Tomoharu Ugawa, and Toshiyuki Maeda
Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency Models
12:30-14:00 lunch break
14:00-15:00 Invited speaker: Shaz Qadeer
On Refining Atomic Actions in the CIVL Program Verifier
Session 7 Concurrency
15:00-15:30 Wytse Oortwijn, Marieke Huisman, Stefan Blom, Marina Zaharieva-Stojanovski, and Dilian Gurov
An Abstraction Technique for Describing Concurrent Program Behaviour

Invited Speakers

Program Chairs

Program Committee

Previous Editions