VSTTE 2015

7th Working Conference on Verified Software: Theories, Tools, and Experiments
San Francisco, California, USA
July 18 - 19, 2015
Co-located with 25th Conference on Computer Aided Verification (http://i-cav.org/2015)
Full Paper Submission Deadline: April 27, 2015 May 1, 2015

Overview | Program | Paper Submissions | Important Dates | Organization & Program Committee


The Seventh Working Conference on Verified Software: Theories, Tools, and Experiments follows a successful inaugural working conference at Zurich in 2005 followed by conferences in Toronto (2008), Edinburgh (2010), Philadelphia (2012), Atherton (2013) and Vienna (2014). The goal of this conference 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. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We welcome papers describing novel experiments and case studies evaluating verification techniques and technologies. Topics of interest include education, requirements modeling, specification languages, specification/verification 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.


Time Title
July 18
09:00 - 10:00 Invited Talk: Chris Hawblitzel (Microsoft Research), "How much can systems software verification be automated?"
10:00 - 10:30 Break
Session 1
Chair: Chris Hawblitzel
10:30 - 11:00 Jean-Christophe Filliatre, Andrei Paskevich and Martin Clochard, How to Avoid Proving the Absence of Integer Overflows
11:00 - 11:30 Felix Dörre and Vladimir Klebanov, Pseudo-Random Number Generator Verification - A Case Study
11:30 - 12:00 Eric Smith and Alessandro Coglio, Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover
12:00 - 13:30 Lunch
Session 2
Chair: Martin Schaef
13:30 - 14:00 Achim D. Brucker, Oto Havle, Yakoub Nemouchi and Burkhart Wolff, Testing the IPC Protocol for a Real-Time Operating System
14:00 - 14:30 Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi and Priya Narasimhan, AUSPICE: Automatic Safety Property Verification for Unmodified Executables
14:30 - 15:00 Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn and Wolfgang Reif, Inside a Verified Flash File System: Transactions & Garbage Collection
15:00 - 15:30 Break
Session 3
Chair: Nikolaj Bjorner
15:30 - 16:00 Jonas Oberhauser, New Techniques for Store Buffer Reduction
16:00 - 16:30 Wojciech Mostowski, Dynamic Frames Based Verification Method for Concurrent Java Programs
16:30 - 17:00 Andreas Katis, Andrew Gacek and Michael W. Whalen, Machine-Checked Proofs For Realizability Checking Algorithms
July 19
09:00 - 10:00 Invited Talk: Lee Pike (Galois Inc.), "Programming Languages for High-Assurance Autonomous Vehicles"
10:00 - 10:30 Break
Session 4
Chair: Jyotirmoy Deshmukh
10:30 - 11:00 Tewodros A. Beyene, Andrey Rybalchenko, Corneliu Popeea and Swarat Chaudhuri, Recursive Games for Compositional Program Synthesis
11:00 - 11:30 Leonardo Alt, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina, A Proof-Sensitive Approach for Small Propositional Interpolants
11:30 - 12:00 Ali Sezgin and Serdar Tasiran, Moving Around: Lipton's Reduction for TSO
12:00 - 13:30 Lunch
13:30 - 15:00 Panel Discussion on "Software Verification Competitions: Lessons Learned and Challenges Ahead"
Domagoj Babic, Dirk Beyer, Alberto Griggio, Vladimir Klebanov, Andrey Rybalchenko, Michael Tautschnig
15:00 - 15:30 Break
15:30 - 16:00 Conclusion of Panel, and Conference Wrap-up

Paper Submissions

Papers will be evaluated by at least three members of the Program Committee. We are accepting both long (limited to 16 pages) and short (limited to 10 pages) paper submissions, written in English. 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.

Research paper submissions must be in LNCS format and must include a cogent and self-contained description of the ideas, methods, results, and comparison to existing work. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains.

Papers should be submitted through: https://www.easychair.org/conferences/?conf=vstte2015.

Submissions that arrive late, are not in the proper format, or are too long will not be considered. The post-conference proceedings of VSTTE 2015 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, obtainable from http://www.springer.de/comp/lncs/authors.html, is strongly encouraged.


Accepted papers will be published as post-Proceedings, to appear in Springer's Lectures Notes in Computer Science.

Important Dates

Abstract submission: April 20, 2015 April 27, 2015
Full paper submission: April 27, 2015 May 1, 2015
Notification: June 8, 2015 June 10, 2015


General Chair: Martin Schaef (SRI International)
Program Chairs: Arie Gurfinkel (CMU SEI) and Sanjit A. Seshia (UC Berkeley)
Publicity Chair: Daniel Bundala (UC Berkeley)

Program Committee:

Elvira Albert (Complutense University of Madrid)
Nikolaj Bjorner (Microsoft Research)
Evan Chang (University of Colorado, Boulder)
Ernie Cohen (Amazon)
Jyotirmoy Deshmukh (Toyota)
Jin Song Dong (National University of Singapore)
Vijay D'Silva (Google)
Vijay Ganesh (University of Waterloo)
Alex Groce (Oregon State)
Arie Gurfinkel (Software Engineering Institute, Carnegie Mellon University) (co-chair)
Bill Harris (Georgia Institute of Technology)
Chris Hawblitzel (Microsoft Research)
Bart Jacobs (Katholieke Universiteit Leuven, Belgium)
Susmit Jha (United Technologies)
Rajeev Joshi (Laboratory for Reliable Software, Jet Propulsion Laboratory)
Vladimir Klebanov, Karlsruhe Institute of Technology, DE
Akash Lal (Microsoft Research India)
Ruzica Piskac (Yale)
Zvonimir Rakamaric (University of Utah)
Kristin Yvonne Rozier (University of Cincinnati)
Sanjit A. Seshia (UC Berkeley) (co-chair)
Natarajan Shankar (SRI)
Carsten Sinz (KIT)
Nishant Sinha (IBM Research Labs)
Alexander Summers (ETH Zurich)
Zachary Tatlock (University of Washington)
Sergey Tverdyshev (Sysgo AG)
Arnaud Venet (CMU / NASA Ames Research Center)
Karen Yorav (IBM Haifa Research Lab)

Contact vstte2015@easychair.org for further information