VSTTE 2018

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

July 18-19, 2018, Oxford, UK
Affiliated with the 30th International Conference on Computer-Aided Verification (CAV 2018).
Part of the Federated Logic Conference style=, local information can be found here.


Submissions | Important Dates | Program | Program Chairs | Program Committee | Previous Editions

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 2018 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 2017 will be published in the Lecture Notes in Computer Science (LNCS) series. Authors of accepted papers will be requested to sign the copyright transfer form.

Call for papers.

Program

Wednesday, July 18

9:00-10:00 Invited speaker: Cesare Tinelli
Contract-based Compositional Verification of Infinite-State Reactive Systems

Abstract: Model-based software development is a leading methodology for the construction of safety- and mission-critical embedded systems. Formal models of such systems can be validated, via formal verification or testing, against system-level requirements and modified as needed before the actual system is built. In many cases, source code can be even produced automatically from the model once the system designer is satisfied with it. As embedded systems become increasingly large and sophisticated the size and complexity of models grows correspondingly, making the verification of top-level requirements harder, especially in the case of infinite-state systems. We argue that, as with conventional software, contracts are an effective mechanism to establish boundaries between components in a system model, and can be used to aid the verification of system-level properties by using compositional reasoning techniques. Component-level contracts also enable formal analyses that provide more accurate feedback to identify sources of errors or the parts of a system that contribute to the satisfaction of a given requirement. This talk discusses our experience in designing an assume-guarantee-based contract language on top of the Lustre modeling language and leveraging it to extend the Kind 2 model checker with contract-based compositional reasoning techniques.

Abstract: Cesare Tinelli received a Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign in 1999 and is currently a full professor in Computer Science at the University of Iowa. Professor Tinelli has done seminal work in automated reasoning, in particular in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His work has appeared in more than 80 refereed publications and has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, NSF, and ONR) and corporations (Intel, General Electric, Rockwell Collins, and United Technologies). He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He has led the development of the award winning Darwin theorem prover and the Kind 1 and Kind 2 model checkers which has found users in the avionics and automotive industries. He has co-led the development of the widely used and award winning CVC3 and CVC4 SMT solvers. He also co-leads the development of StarExec, a cross community web-based service for the comparative evaluation of logic solvers. He is an associate editor of the Journal of Automated Reasoning and a founder the SMT workshop series and the Midwest Verification Day series. He has served in the program committee of more than 70 automated reasoning and formal methods conferences and workshops, as well as the steering committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15.

Session 1 Model Checking I
10:00-10:30 Jochen Hoenicke, Alexander Nutz and Andreas Podelski
A Tree-Based Approach to Data Flow Proofs
10:30-11:00 coffee break
Session 2 Model Checking II
11:00-11:30 Arie Gurfinkel, Temesghen Kahsai and Jorge A Navas
Executable Counterexamples in Software Model Checking
11:30-12:00 Pritom Rajkhowa and Fangzhen Lin
Extending VIAP to Handle Array Programs
12:00-12:30 Karine Even-Mendoza, Sepideh Asadi, Antti Hyvärinen, Hana Chockler and Natasha Sharygina
Lattice-Based Refinement in Bounded Model Checking
12:30-14:00 lunch break
14:00-15:00 Invited speaker: Stuart Matthews
Verified Software: Theories, Tools, ... and Engineering

Abstract: Continual innovation of software verification theories & tools is essential in order to meet the challenges of ever-more complex software-intensive systems. But achieving impact ultimately requires an understanding of the engineering context in which the tools will be deployed. Based on our tried-and-trusted methods of high-integrity software development at Altran, I will identify key features of the industrial landscape in which software verification tools have to operate, and some of the pitfalls that can stop them being adopted, including regulation, qualification, scalability, cost justification, and the overall tool ecosystem. Within this context I will present Altran's own on-going research & development activities in verified software technologies. The talk will conclude by drawing some key lessons that can be applied to avoid the traps and pitfalls that tools encounter on their journey to succesful deployment.

Bio: Stuart Matthews has over 20 years' experience with high integrity software engineering including the application of formal methods for verification and validation of critical systems. Stuart is currently the head of R&T within the Intelligent Systems Expertise Centre at Altran UK with responsibility for the technology pipeline and a portfolio of on-going research projects. The portfolio includes the SPARK static verification toolset & support services for which Stuart also acts as the product manager at Altran.

Session 3 Certification & Formalisation I
15:00-15:30 Milad Ketab Ghale, Dirk Pattinson and Ramana Kumar
Verified Certificate Checking for Counting Votes
15:30-16:00 coffee break
Session 4 Certification & Formalisation II
16:00-16:30 Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen and Son Ho
Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
16:30-17:00 Brandon Bohrer and Karl Crary
TWAM: A Certifying Abstract Machine for Logic Programs
17:00-17:30 Patryk Czarnik, Jacek Chrząszcz and Aleksy Schubert
A Java bytecode formalisation
17:30-18:00 Paolo Torrini, David Nowak, Narjes Jomaa and Mohamed Sami Cherif
Formalising Executable Specifications of Low-Level Systems
19:15-21:30 Workshop dinner at Magdalen College

Thursday, July 19

9:00-10:00 Invited speaker: Rayna Dimitrova
Synthesis of Surveillance Strategies for Mobile Sensors

Abstract: The increasing application of formal methods to the design of autonomous systems often requires extending the existing specification and modeling formalisms, and addressing new challenges for formal verification and synthesis. In this talk, I will focus on the application of reactive synthesis to the problem of automatically deriving strategies for autonomous mobile sensors conducting surveillance, that is, maintaining knowledge of the location of a moving, possibly adversarial target. By extending linear temporal logic with atomic surveillance predicates, complex temporal surveillance objectives can be formally specified in a way that allows for seamless combination with other task specifications. I will discuss two key challenges for applying state-of-the-art methods for reactive synthesis to temporal surveillance specifications. First, naively keeping track of the knowledge of the surveillance agent leads to a state-space explosion. Second, while sensor networks with a large number of dynamic sensors can achieve better coverage, synthesizing coordinated surveillance strategies is challenging computationally. I will outline how abstraction, refinement, and compositional synthesis techniques can be used to address these challenges.

Bio: Rayna Dimitrova is a Lecturer (Assistant Professor) at the University of Leicester, UK. Prior to that, she held postdoctoral positions at the University of Texas at Austin, and at the Max Planck Institute for Software Systems in Germany. She completed her PhD at Saarland University in Germany. Rayna's research is focused on the specification, verification, and synthesis of reactive systems. She primarily investigates quantitative versions of these questions, centered around the aspect of uncertainty in system and environment models. She is particularly interested in applications of formal methods to autonomous systems, where her work addresses the limitations faced by autonomous control due to imperfect sensing and stochastic disturbances.

Session 5 Certification & Formalisation III
10:00-10:30 Alessandro Coglio
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
10:30-11:00 coffee break
Session 6 Security
11:00-11:30 Robin Adams and Sibylle Schupp
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
11:30-12:00 Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCarthaigh, Daniel Schwartz-Narbonne and Serdar Tasiran
SideTrail: Verifying Time-Balancing of Cryptosystems
12:00-12:30 Jakub Zakrzewski
Towards verification of Ethereum smart contracts: a formalization of core of Solidity
12:30-14:00 lunch break
Session 7 New Applications
14:00-14:30 Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich and Alexander Weigl
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
14:30-15:00 David Cok and Serdar Tasiran
Practical Methods for Reasoning about Java 8's Functional Programming Features
15:00-15:30 Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang and Harald Ruess
Verification of Binarized Neural Networks via Inter-Neuron Factoring
15:30-16:00 coffee break
Session 8 Off the beaten track
16:00-16:30 Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz and Andreas Podelski
The Map Equality Domain
16:30-17:00 Naoki Nishida and Sarah Winkler
Loop Detection by Logically Constrained Term Rewriting
17:00-17:30 Jonas Oberhauser
Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment

Important Dates

Program Chairs

Program Committee

Previous Editions