Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

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.

Dates
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 13 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 1VMCAI at Sala III
Chair(s): Constantin Enea Université Paris Diderot
09:00
90m
Talk
Under and Over Approximated Reachability Analysis for the Verifcation of Control Systems
VMCAI
Sylvie Putot École Polytechnique
14:00 - 15:30
Program SynthesisVMCAI at Sala III
Chair(s): Nuno P. Lopes Microsoft Research
14:00
30m
Talk
Minimal Synthesis of String To String Functions From Examples
VMCAI
Jad Hamza LIAFA, Université Paris Diderot, Viktor Kunčak EPFL, Switzerland
14:30
30m
Talk
Lazy but Effective Functional Synthesis
VMCAI
Grigory Fedyukovich Princeton University, Arie Gurfinkel University of Waterloo, Aarti Gupta Princeton University
15:00
30m
Talk
Automatic Program Repair using Formal Verification and Expression Templates
VMCAI
Thanh-Toan Nguyen , Quang-Trung Ta National University of Singapore, Wei-Ngan Chin National University of Singapore
16:00 - 17:30
Abstract Interpretation (2)VMCAI at Sala III
Chair(s): Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France
16:00
30m
Talk
Demand Control-Flow Analysis
VMCAI
Kimball Germane University of Utah, Jay McCarthy University of Massachusetts Lowell, Michael D. Adams University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School
16:30
30m
Talk
Effect-driven Flow Analysis
VMCAI
Jens Nicolay Vrije Universiteit Brussel, Belgium, Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
17:00
30m
Talk
Relatively Complete Pushdown Analysis of Escape Continuations
VMCAI
Kimball Germane University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School

Mon 14 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 2VMCAI at Sala III
Chair(s): Lenore Zuck
09:00
90m
Talk
Designing Self-Certifying Software Systems
VMCAI
Kedar Namjoshi Bell Labs, Nokia
11:00 - 12:30
Decision ProceduresVMCAI at Sala III
Chair(s): Kedar Namjoshi Bell Labs, Nokia
11:00
30m
Talk
Solving and Interpolating Constant Arrays Based on Weak Equivalences
VMCAI
Jochen Hoenicke Universität Freiburg, Tanja Schindler University of Freiburg
11:30
30m
Talk
A Decidable Logic for Tree Data-Structures with Measurements
VMCAI
Xiaokang Qiu Purdue University, Yanjun Wang Purdue University
File Attached
12:00
30m
Talk
A Practical Algorithm for Structure Embedding
VMCAI
Charlie Murphy Princeton University, Zachary Kincaid Princeton University
File Attached
14:00 - 15:30
Probabilistic SystemsVMCAI at Sala III
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
14:00
30m
Talk
Syntactic Partial Order Compression for Probabilistic Reachability
VMCAI
Gereon Fox , Daniel Stan , Holger Hermanns Saarland University
14:30
30m
Talk
Termination of Nondeterministic Probabilistic Programs
VMCAI
Hongfei Fu IST Austria, Krishnendu Chatterjee IST Austria
15:00
30m
Talk
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
VMCAI
Stefan Haar , Juraj Kolčák LSV, CNRS & ENS Cachan, University Paris Saclay, Loïc Paulevé

Tue 15 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 3VMCAI at Sala III
Chair(s): Ruzica Piskac Yale University, USA
09:00
90m
Talk
Semantics for Compiler IRs: Undefined Behavior is not Evil!
VMCAI
Nuno P. Lopes Microsoft Research
Media Attached
11:00 - 12:30
Software Verification and SynthesisVMCAI at Sala III
Chair(s): Ori Lahav Tel Aviv University
11:00
30m
Talk
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
VMCAI
Viorel Preoteasa , Iulia Dragomir , Stavros Tripakis Aalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
11:30
30m
Talk
euforia: Complete Software Model Checking with Uninterpreted Functions
VMCAI
12:00
30m
Talk
Program Synthesis with Equivalence Reduction
VMCAI
Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison
14:00 - 15:30
Software VerificationVMCAI at Sala III
Chair(s): Grigory Fedyukovich Princeton University
14:00
30m
Talk
Type-directed Bounding of Collections in Reactive Programs
VMCAI
Tianhan Lu University of Colorado Boulder, Pavol Cerny University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder, Ashutosh Trivedi
14:30
30m
Talk
Exploiting Pointer Analysis in Memory Models for Deductive Verification
VMCAI
Quentin Bouillaguet , François Bobot CEA, Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France, Boris Yakobowski CEA - LIST
File Attached
15:00
30m
Talk
Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
VMCAI
Anja Karl Institute of Applied Information Processing and Communications, Graz University of Technology, Robert Schilling , Roderick Bloem Institute of Software Technology, Graz University of Technology , Stefan Mangard
16:00 - 17:30
Networks and ConcurrencyVMCAI at Sala III
Chair(s): Cezara Drăgoi INRIA, ENS, CNRS
16:00
30m
Talk
On the Semantics of Snapshot Isolation
VMCAI
Azalea Raad MPI-SWS, Germany, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
16:30
30m
Talk
Fast BGP Simulation of Large Datacenters
VMCAI
Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research
Pre-print
17:00
30m
Talk
Parametric Timed Broadcast Protocols
VMCAI
Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye , Paulin Fournier , Didier Lime
File Attached

Accepted Papers

Title
A Decidable Logic for Tree Data-Structures with Measurements
VMCAI
File Attached
A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
VMCAI
File Attached
Application of Abstract Interpretation to the Automotive Electronic Control System
VMCAI
A Practical Algorithm for Structure Embedding
VMCAI
File Attached
Automatic Program Repair using Formal Verification and Expression Templates
VMCAI
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
VMCAI
Demand Control-Flow Analysis
VMCAI
Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis
VMCAI
File Attached
Effect-driven Flow Analysis
VMCAI
euforia: Complete Software Model Checking with Uninterpreted Functions
VMCAI
Exploiting Pointer Analysis in Memory Models for Deductive Verification
VMCAI
File Attached
Fast BGP Simulation of Large Datacenters
VMCAI
Pre-print
Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic
VMCAI
Lazy but Effective Functional Synthesis
VMCAI
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
VMCAI
Link to publication DOI Pre-print File Attached
Minimal Synthesis of String To String Functions From Examples
VMCAI
On the Semantics of Snapshot Isolation
VMCAI
Parametric Timed Broadcast Protocols
VMCAI
File Attached
Program Synthesis with Equivalence Reduction
VMCAI
Relatively Complete Pushdown Analysis of Escape Continuations
VMCAI
Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
VMCAI
Solving and Interpolating Constant Arrays Based on Weak Equivalences
VMCAI
Static Analysis of Binary Code with Memory Indirections Using Polyhedra
VMCAI
File Attached
Syntactic Partial Order Compression for Probabilistic Reachability
VMCAI
Termination of Nondeterministic Probabilistic Programs
VMCAI
Type-directed Bounding of Collections in Reactive Programs
VMCAI
Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking
VMCAI

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.