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

News: The proceedings of VSTTE 2017 are now available on-line.
The access is open for all VSTTE participants till January 19, 2018.

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.

Program

Saturday, July 22

9:00-10:00 Invited speaker: Santiago Zanella-Beguelin
Everest: a Verified and High-Performance HTTPS Stack

The HTTPS ecosystem is the foundation of Internet security, with the TLS protocol and numerous cryptographic constructions at its core. Unfortunately, this ecosystem is extremely brittle, with frequent emergency patches and headline-grabbing attacks (e.g. Heartbleed, Logjam, Freak). The Everest expedition, joint between Microsoft Research, Inria and CMU, is a 5-year large-scale verification effort aimed at solving this problem by constructing a machine-checked, high-performance, standards-compliant implementation of the full HTTPS ecosystem. This talk is a report on the progress after just over one year into our expedition, and will overview the various verification tools that we use and their integration, including:

  • F*, a dependently-typed ML-like language for programming and verification at high level;
  • Low*, a subset of F* designed for C-like imperative programming;
  • KreMLin, a compiler toolchain that extracts Low* programs to C;
  • Vale, an extensible macro assembly language that uses F* as a verification backend.

Our flagship project is miTLS, a reference implementation of TLS using cryptographic components programmed and verified in F*, Low* and Vale. We compile all our code to source quality C and assembly, suitable for independent audit and deployment. miTLS supports the latest TLS 1.3 standard, including Zero Round-Trip Time (0-RTT) resumption, and has been integrated in libcurl and the nginx web server.

Session 1 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 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

An automated reasoning system is the implementation of an algorithm that adds a strategy to a calculus that is based on a logic. Typically, automated reasoning systems "solve" NP-hard problems or beyond. Therefore, I argue that automated reasoning system need often to be specific to a given problem. The combination of a system and a problem is called an application.

In the talk I discuss design principles based on this layered view of automated reasoning systems and their applications. I select and discuss design principles from all six layers: application, system, implementation, algorithm, calculus, and logic.

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 Hoffmann
Why Verification Cannot Ignore Resource Usage

Verified programs only execute as specified if a sufficient amount of resources, such as time and memory, is available at runtime. Moreover, resource usage is often directly connected to correctness and security properties that we wish to verify. This talk will show examples of such connections and present recent work on automatic inference and verification of resource-usage bounds for functional and imperative programs. These automatic methods can be combined with other verification techniques to provide stronger guarantees at runtime.

Session 5 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 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
Constructing Correct Concurrent Programs Layer by Layer

CIVL is a refinement-oriented verifier for concurrent programs implemented as a conservative extension to the Boogie verification system. CIVL allows the proof of correctness of a concurrent program — shared-memory or message-passing — to be described as a sequence of program layers. The safety of a layer implies the safety of the layer just below, thus allowing the safety of the highest layer to transitively imply the safety of the lowest.

The central theme in CIVL is reasoning about atomic actions. Different layers of a program describe the behavior of the program using atomic actions, higher layers with coarse-grained and lower layers with fine-grained atomic actions. The formal and automated verification justifying the connection among layers combines several techniques — linear variables, reduction based on movers, location invariants, and procedure-local abstraction.

CIVL is available in the master branch of Boogie together with more than fifty micro-benchmarks. CIVL has also been used to refine a realistic concurrent garbage collection algorithm from a simple high-level specification down to a highly-concurrent implementation described in terms of individual memory accesses.

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