VMCAI 2019 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation

Welcome to the website of the International Conference on Verification, Model Checking, and Abstract Interpretation 2019.

VMCAI provides a forum for researchers from the communities of Verification, Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. VMCAI 2019 will be the 20th edition in the series.

VMCAI Winter School

This year we are organizing for the first time a winter school before the VMCAI conference. The winter school will take place during the period January 9-12th, 2018.

The registration is free but it is mandatory. Please take into consideration that the number of attendees is limited. Register as soon you are sure to be able to attend the Winter School. The registration deadline for the winter school is December 22, 2018. More details at http://vmcaischool19.tecnico.ulisboa.pt.

The VMCAI Winter School program will feature two tutorial lectures per day, presented by distinguished speakers and experts in these fields.

List of tutorial lectures:

• An Introduction to Learning from Programs, by Marc Brockschmidt (Microsoft Research, Cambridge, UK)

• Models and Techniques for Analyzing Security Protocols, by Veronique Cortier (Loria, Nancy, France)

• Neural Network Verification, by M. Pawan Kumar (University of Oxford, UK)

• Computing with SAT Oracles: From CDCL SAT Solving to Ubiquitous Industry Adoption, by João Marques-Silva (University of Lisbon, Portugal)

• Abstract Interpretation, by Patrick Cousot (New York University, USA). This tutorial will be complemented by an invited talk by Sylvie Putot (Ecole Polytechnique, France) on Zonotopic abstract domains for numerical program analysis.

• Developing distributed protocols formally with Ivy, by Ken McMillan (Microsoft Research, Redmond, USA). This tutorial will be complemented by an invited talk by Kedar Namjoshi (Nokia Bell Labs,USA) on Modular Verification: Model Checking in Bits and Pieces.

Accepted Papers

Best Paper Award

Congratulations to Clément Ballabriga, Julien Forget, Laure Gonnord, Giuseppe Lipari and Jordy Ruiz for winning the best paper award for their paper “Static Analysis of Binary Code with Memory Indirections Using Polyhedra” !

This award is sponsored by Springer.

Invited Speakers

Nuno P. Lopes (Microsoft Research): Semantics for Compiler IRs: Undefined Behavior is not Evil!

Abstract: Building a compiler IR is tricky. First, it should be efficient to compile the desired source language to this IR. Second, the IR should support all the desired optimizations and analyses, and these should run efficiently. Finally, it should be possible to lower this IR into the desired target assembly efficiently. Striking a good tradeoff in this design space isn’t easy.

Undefined behavior (UB) has been used in production compilers’ IRs for a long time. In this talk, we will explore what’s UB, what it achieves, why it may be a good idea, and why it is not as evil as most people think it is.

Bio: Nuno Lopes is a researcher at MSR Cambridge. He holds a PhD from the University of Lisbon, and has previously interned at MSR Redmond, Apple, Max Planck Institute (MPI-SWS), and the Institute for Systems and Robotics (ISR) Lisbon. Nuno’s interests include software verification, compilers, and mixing the two.

Kedar Namjoshi (Nokia Bell Labs): Designing Self-Certifying Software Systems

Abstract: Large software systems are hard to understand. The size and complexity of the implementation, possibly written in a mix of programming languages; a large number of potential configurations; concurrency and distribution, all contribute to the difficulty of precisely analyzing system behavior. How can one have confidence in the correct working of such a complex system?

In this talk, I will explore an unusual approach to this challenge. Suppose that the software system is designed so that it produces a mathematical certificate to justify the correctness of its result. The behavior of such a “self-certifying” system can then be formally verified at run time, by checking the validity of each certificate as it is generated, without having to examine or reason directly about the system implementation. Self-certification thus shrinks the size of the trusted computing base, often by orders of magnitude, as only the certificate checker must be trusted.

The central research question is to design a certificate format which is comprehensive, easy to generate, and straightforward to check. I will sketch how this may be done for a variety of software system types: model checkers and static analyzers, network operating systems, and optimizing compilers. I will also discuss intriguing open questions and talk about some of the unexpected benefits of certification.

Bio: Kedar Namjoshi is a member of technical staff at Nokia Bell Labs in Murray Hill, NJ. He received his Ph.D. from the University of Texas at Austin with E. Allen Emerson, and the B.Tech. degree from the Indian Institute of Technology, Madras, both in the Computing Sciences. His research interests include program semantics, logics and verification, model checking, static program analysis, distributed computing, and programming methodology.

Sylvie Putot (Ecole Polytechnique): Under and over approximated reachability analysis for the verifcation of control systems

Abstract: This talk will present a class of methods to compute under and over approximating flowpipes for differential systems, possibly with delays, systems that are pervasive in the modeling networked control systems. Computing over-approximations of the reachable states has become a classical tool for the safety verification of control systems. Under-approximations are notoriously more difficult to compute, and their use for verification much less studied. We will discuss the guarantees and properties that can be obtained from the joint use of these under and over-approximations for control systems with inputs and disturbances.

Bio: Sylvie Putot is Professor in the Department of Computer Science of Ecole Polytechnique. Her research focuses on set-based methods and abstractions for the verification of numerical programs and more generally cyber-physical systems. She is also one of the main authors of the Fluctuat static analyzer, dedicated to the analysis of floating-point programs.

Call for Papers

VMCAI 2019 welcomes research papers on any topic related to verification, model checking, and abstract interpretation. Research contributions can report new results as well as experimental evaluations and comparisons of existing techniques. Topics include, but are not limited to: Program Verification, Model Checking, Abstract Interpretation, Abstract Domains, Program Synthesis, Static Analysis, Type Systems, Deductive Methods, Program Logics, First-Order Theories, Decision Procedures, Interpolation, Horn Clause Solving, Program Certification, Separation Logic, Probabilistic Programming and Analysis, Error Diagnosis, Detection of Bugs and Security Vulnerabilities, Program Transformations, Hybrid and Cyber-physical Systems, Concurrent Systems, Analysis of Numerical Properties.

Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, and object-oriented programming.

Submissions

Submissions are restricted to 20 pages in Springer’s LNCS format, not counting references. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website.

Submissions must be uploaded via the paper submission site.

Accepted papers will be published in Springer’s Lecture Notes in Computer Science series.

Proceedings

The proceedings is freely available here until February 28th. After that date you can access the proceedings on their Springer website.