VSTTE 2020

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

July 20-21, 2020, Los Angeles, USA
Co-located with the International Conference on Computer-Aided Verification (CAV 2020) and the International Symposium on Software Testing and Analysis (ISSTA 2020)

Submissions | Important Dates | Registration | Program | Invited Speakers | Program Chairs | Program Committee | Previous Editions

Overview

News: VSTTE 2020 will take place as a virtual meeting.

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.

The Verified Software Initiative (VSI), spearheaded by Tony Hoare and Jayadev Misra, is an ambitious research program for making large-scale verified software a practical reality. The Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE) is the main forum for advancing the initiative. VSTTE brings together experts spanning the spectrum of software verification in order to foster international collaboration on the critical research challenges. The theoretical work includes semantic foundations and logics for specification and verification, and verification algorithms and methodologies. The tools cover specification and annotation languages, program analyzers, model checkers, interactive verifiers and proof checkers, automated theorem provers and SAT/SMT solvers, and integrated verification environments. The experimental work drives the research agenda for theory and tools by taking on significant specification/verification exercises covering hardware, operating systems, compilers, computer security, parallel computing, and cyber-physical systems.

The 2020 edition of VSTTE will be the 12th working conference in the series, and will be co-located with CAV 2020 and ISSTA 2020 in Los Angeles, USA.

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, but are not limited to, 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.

Work on diverse verification technologies, e.g., static analysis, dynamic analysis, model checking, theorem proving, satisfiability, is particularly encouraged.

Paper Submissions

VSTTE 2020 will accept both long (limited to 16 pages, excluding references) and short (limited to 10 pages, excluding references) 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. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains.

Papers will be submitted via EasyChair at the VSTTE 2020 conference page. Submissions that arrive late, are not in the proper format, or are too long will not be considered. The post-conference proceedings of VSTTE 2020 will be published by Springer-Verlag in the LNCS series. Authors of accepted papers will be requested to sign a form transferring copyright of their contribution to Springer-Verlag. The use of LaTeX and the Springer LNCS class files is strongly encouraged.

Program

Monday, July 20

PDT Session 1: Static analysis and verified compilation
5:30-5:50 Pietro Ferrara and Luca Negrini
SARL: OO Framework Specification for Static Analysis
5:50-6:10 Marko Kleine Büning, Carsten Sinz and David Farago
QPR Verify: A Static Analysis Tool for Embedded Software based on Bounded Model Checking
6:10-6:30 Vadim Zaliva, Ilia Zaichuk and Franz Franchetti
Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX
PDT Session 2: Invited talk
7:00-8:00 Bor-Yuh Evan Chang (University of Colorado Boulder and Amazon, USA)
Goal-Directed Static Analysis and Software Frameworks

Slides

Abstract: Static analysis is about computing a global over-approximation of a program's behavior from its source code. But what if most of its code is missing or unknown? Analyzing app code developed against modern software frameworks for mobile or the web is essentially this situation. To create apps that behave as expected, developers must follow complex and often implicit programming protocols imposed by the framework. So what makes static analysis of apps hard is largely what makes programming them hard: the specification of the programming protocol is unclear, and the control flow is complex, asynchronous, dynamic, and higher-order. In this talk, I present some of our efforts in developing tools and techniques for analyzing such code motivated by real-world application domains. In particular, in such situations, we have seen benefits to moving our focus beyond the global reasoning engine to apply goal-directed analysis in support of tasks like alarm triage, demand-driven refinement, and evidence generation.

Bio: Bor-Yuh Evan Chang is an Associate Professor of Computer Science at the University of Colorado Boulder and an Amazon Scholar. He is interested in tools and techniques for building, understanding, and ensuring reliable computational systems. His techniques target using novel ways of interacting with the programmer to design more precise and practical program analyses. He is a recipient of an NSF CAREER award (2010).
PDT Session 3: Invited talk
10:45-11:45 Isil Dillig (The University of Texas at Austin, USA)
Formal Methods for Database Application Evolution

Slides

Abstract: Database applications typically undergo several schema changes during their life cycle due to performance and maintainability reasons. Such changes to the database schema not only require migrating the underlying data to a new schema but also re-implementing large chunks of the application code that query and update the database. In this talk, we describe how formal methods can simplify (and ensure the correctness of) evolving database applications. Specifically, we first describe our work on verifying equivalence between database applications that operate over different schema, such as those that arise before and after schema refactoring. Next, we describe how to use this verification procedure to solve the corresponding synthesis problem: That is, given a database application and a new schema, how can we automatically generate an equivalent program over this new schema?

Bio: Isil Dillig is an associate professor at the computer science department of the University of Texas at Austin where she leads the UToPiA research group. Her main research interests are program analysis and verification, program synthesis, and automated logical reasoning. She obtained all her degrees (BS, MS, PhD) at Stanford University. Isil is a 2015 Sloan Fellow and a recipient of an NSF CAREER award.

Tuesday, July 21

PDT Session 1: Synthesis, repair, and testing
5:30-5:50 Konstantinos Athanasiou, Thomas Wahl, A. Adam Ding and Yunsi Fei
Automatic Detection and Repair of Transition-Based Leakage in Software Binaries
5:50-6:10 Joseph Scott, Federico Mora and Vijay Ganesh
BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers
6:10-6:30 Alessandro Trindade and Lucas Cordeiro
Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison
PDT Session 2: Quantitative program analysis and cryptography
7:00-7:20 Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno and Chris Hawblitzel
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
7:20-7:40 Abtin Molavi, Thomas Schneider, Mara Downing and Lucas Bang
MCBAT: Model Counting for Constraints over Bounded Integer Arrays
7:40-8:00 Jorge Navas, Bruno Dutertre and Ian Mason
Verification of an Optimized NTT Algorithm
PDT Session 3: Invited talk
10:45-11:45 Xi Wang (University of Washington, USA)
Automated Verification of Systems Software with Serval

Slides

Abstract: This talk will give an overview of Serval, a framework for developing automated verifiers for systems software. Serval builds on the Rosette solver-aided language to provide an extensible infrastructure for creating verifiers by lifting interpreters under symbolic evaluation, and a systematic approach to identifying and repairing verification performance bottlenecks using symbolic profiling and optimizations. Using Serval, we build automated verifiers for the RISC-V, ARM, x86, LLVM, and BPF instruction sets. We report our experience of retrofitting CertiKOS and Komodo, two systems previously verified using Coq and Dafny, respectively, for automated verification using Serval. In addition, we apply Serval to the BPF just-in-time compilers in the Linux kernel, uncovering more than 30 new bugs.

Bio: Xi Wang is an associate professor in the Paul G. Allen School of Computer Science & Engineering at the University of Washington. He received his PhD from MIT, and B.E. and M.E. from Tsinghua. His research interests are in building secure and reliable systems. He contributed to the STACK tool for finding undefined behavior bugs in C programs, the Yggdrasil toolkit for writing file systems with push-button verification, and the Serval framework for automated verification of systems software.

Important Dates

Registration

Registration to VSTTE is free and part of the CAV registration process. Registration is open until July 10, 2020.

Invited Speakers

General Chair

Program Chairs

Program Committee

Previous Editions