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

Sun 13 Jan

VMCAI-2019
09:00 - 10:30: VMCAI 2019 - Invited Talk 1 at Sala III
Chair(s): Constantin EneaUniversité Paris Diderot
VMCAI-201909:00 - 10:30
Talk
Sylvie PutotÉcole Polytechnique
VMCAI-2019
14:00 - 15:30: VMCAI 2019 - Program Synthesis at Sala III
Chair(s): Nuno P. LopesMicrosoft Research
VMCAI-201914:00 - 14:30
Talk
Jad HamzaLIAFA, Université Paris Diderot, Viktor KuncakEPFL, Switzerland
VMCAI-201914:30 - 15:00
Talk
Grigory FedyukovichPrinceton University, Arie GurfinkelUniversity of Waterloo, Aarti GuptaPrinceton University
VMCAI-201915:00 - 15:30
Talk
Thanh-Toan Nguyen, Quang-Trung TaNational University of Singapore, Wei-Ngan ChinNational University of Singapore
VMCAI-2019
16:00 - 17:30: VMCAI 2019 - Abstract Interpretation (2) at Sala III
Chair(s): Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France
VMCAI-201916:00 - 16:30
Talk
Kimball GermaneUniversity of Utah, Jay McCarthyUniversity of Massachusetts Lowell, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School
VMCAI-201916:30 - 17:00
Talk
Jens NicolayVrije Universiteit Brussel, Belgium, Quentin StiévenartVrije Universiteit Brussel, Belgium, Wolfgang De MeuterVrije Universiteit Brussel, Coen De RooverVrije Universiteit Brussel
VMCAI-201917:00 - 17:30
Talk
Kimball GermaneUniversity of Utah, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School

Mon 14 Jan

VMCAI-2019
09:00 - 10:30: VMCAI 2019 - Invited Talk 2 at Sala III
Chair(s): Lenore Zuck
VMCAI-201909:00 - 10:30
Talk
Kedar NamjoshiBell Labs, Nokia
VMCAI-2019
11:00 - 12:30: VMCAI 2019 - Decision Procedures at Sala III
Chair(s): Kedar NamjoshiBell Labs, Nokia
VMCAI-201911:00 - 11:30
Talk
Jochen HoenickeUniversität Freiburg, Tanja SchindlerUniversity of Freiburg
VMCAI-201911:30 - 12:00
Talk
Xiaokang QiuPurdue University, Yanjun WangPurdue University
File Attached
VMCAI-201912:00 - 12:30
Talk
Charlie MurphyPrinceton University, Zachary KincaidPrinceton University
File Attached
VMCAI-2019
14:00 - 15:30: VMCAI 2019 - Probabilistic Systems at Sala III
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA
VMCAI-201914:00 - 14:30
Talk
VMCAI-201914:30 - 15:00
Talk
Hongfei FuIST Austria, Krishnendu ChatterjeeIST Austria
VMCAI-201915:00 - 15:30
Talk
Stefan Haar, Juraj KolčákLSV, CNRS & ENS Cachan, University Paris Saclay, Loïc Paulevé

Tue 15 Jan

VMCAI-2019
09:00 - 10:30: VMCAI 2019 - Invited Talk 3 at Sala III
Chair(s): Ruzica PiskacYale University, USA
VMCAI-201909:00 - 10:30
Talk
Nuno P. LopesMicrosoft Research
VMCAI-2019
11:00 - 12:30: VMCAI 2019 - Software Verification and Synthesis at Sala III
Chair(s): Ori LahavTel Aviv University
VMCAI-201911:00 - 11:30
Talk
Viorel Preoteasa, Iulia Dragomir, Stavros TripakisAalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
VMCAI-201911:30 - 12:00
Talk
VMCAI-201912:00 - 12:30
Talk
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison
VMCAI-2019
14:00 - 15:30: VMCAI 2019 - Software Verification at Sala III
Chair(s): Grigory FedyukovichPrinceton University
VMCAI-201914:00 - 14:30
Talk
Tianhan LuUniversity of Colorado Boulder, Pavol CernyUniversity of Colorado Boulder, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Ashutosh Trivedi
VMCAI-201914:30 - 15:00
Talk
Quentin Bouillaguet, François BobotCEA, Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France, Boris YakobowskiCEA - LIST
File Attached
VMCAI-201915:00 - 15:30
Talk
Anja KarlInstitute of Applied Information Processing and Communications, Graz University of Technology, Robert Schilling, Roderick BloemInstitute of Software Technology, Graz University of Technology , Stefan Mangard
VMCAI-2019
16:00 - 17:30: VMCAI 2019 - Networks and Concurrency at Sala III
Chair(s): Cezara DrăgoiINRIA, ENS, CNRS
VMCAI-201916:00 - 16:30
Talk
Azalea RaadMPI-SWS, Germany, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, Germany
VMCAI-201916:30 - 17:00
Talk
Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research
VMCAI-201917:00 - 17:30
Talk
Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye, Paulin Fournier, Didier Lime
File Attached

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.

Accepted Papers

Title
File Attached
File Attached
File Attached
File Attached
File Attached
Link to publication DOI Pre-print File Attached
File Attached
File Attached