VMCAI
Sun 17 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)

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

Sun 17 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:50 - 09:00
WelcomeVMCAI at Room St Petersburg I
Chair(s): K. Rustan M. Leino Microsoft Research
09:00 - 10:00
Invited Talk IVMCAI at Room St Petersburg I
Chair(s): Sharon Shoham
09:00
60m
Talk
Automating Abstract Interpretation
VMCAI
Thomas Reps University of Wisconsin - Madison and Grammatech Inc.

Mon 18 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Invited Talk IIVMCAI at Room St Petersburg I
Chair(s): K. Rustan M. Leino Microsoft Research
09:00
60m
Talk
Ironclad - Full Verification of Complex Systems
VMCAI
Bryan Parno Microsoft Research
10:30 - 12:00
Hybrid and Timed SystemsVMCAI at Room St Petersburg I
Chair(s): David Monniaux CNRS, VERIMAG
10:30
30m
Talk
Abstract Interpretation with Infinitesimals
VMCAI
Kengo Kido , Swarat Chaudhuri Rice University, Ichiro Hasuo University of Tokyo
11:00
30m
Talk
Lipschitz Robustness of Timed I/O Systems
VMCAI
Thomas A. Henzinger IST Austria, Jan Otop University of Wrocław, Roopsha Samanta IST Austria
11:30
30m
Talk
A method for invariant generation for polynomial continuous systems
VMCAI
Andrew Sogokon , Khalil Ghorbal Carnegie Mellon University, Paul Jackson , André Platzer
14:00 - 15:30
Dynamic and Static VerificationVMCAI at Room St Petersburg I
Chair(s): Aarti Gupta Princeton University
14:00
30m
Talk
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
VMCAI
Pavel Parizek Charles University in Prague
14:30
30m
Talk
Cloud-Based Verification of Concurrent Software
VMCAI
15:00
30m
Talk
Abstraction-driven Concolic Testing
VMCAI

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Invited Talk IIIVMCAI at Room St Petersburg I
Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder
09:00
60m
Talk
Viper - A Verification Infrastructure for Permission-based Reasoning
VMCAI
Peter Müller ETH Zurich
10:30 - 12:00
Concurrent ProgramsVMCAI at Room St Petersburg I
Chair(s): Noam Rinetzky
10:30
30m
Talk
Pointer Race Freedom
VMCAI
Frédéric Haziza , Lukáš Holík , Roland Meyer , Sebastian Wolff Fraunhofer ITWM and TU Kaiserslautern
11:00
30m
Talk
A program logic for C11 memory fences
VMCAI
Marko Doko MPI-SWS, Germany, Viktor Vafeiadis MPI-SWS, Germany
11:30
30m
Talk
From Low Level Pointers to High Level Containers
VMCAI
Kamil Dudka , Lukáš Holík , Petr Peringer , Tomáš Vojnar Brno University of Technology
14:00 - 15:30
Parameterized and Component-Based SystemsVMCAI at Room St Petersburg I
Chair(s): Arie Gurfinkel Carnegie Mellon University
14:00
30m
Talk
Regular Symmetry Patterns
VMCAI
Anthony Widjaja Lin Yale-NUS College, Singapore, Truong Khanh Nguyen , Philipp Ruemmer Uppsala University, Jun Sun
14:30
30m
Talk
Tight Cutoffs for Guarded Protocols with Fairness
VMCAI
15:00
30m
Talk
A General Modular Synthesis Problem for Pushdown Systems
VMCAI

Accepted Papers

Title
Abstract Interpretation with Infinitesimals
VMCAI
Abstraction-driven Concolic Testing
VMCAI
A General Modular Synthesis Problem for Pushdown Systems
VMCAI
A method for invariant generation for polynomial continuous systems
VMCAI
An Abstract Domain of Uninterpreted Functions
VMCAI
A program logic for C11 memory fences
VMCAI
Automatic Generation of Propagation Complete SAT Encodings
VMCAI
Cloud-Based Verification of Concurrent Software
VMCAI
D3 : Data-Driven Disjunctive Abstraction
VMCAI
Exact Heap Summaries for Symbolic Execution
VMCAI
From Low Level Pointers to High Level Containers
VMCAI
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
VMCAI
Lazy Constrained Monotonic Abstraction
VMCAI
Lipschitz Robustness of Timed I/O Systems
VMCAI
Model Checking with Multi-Threaded IC3 Portfolios
VMCAI
Parameter Synthesis for Parametric Interval Markov Chains
VMCAI
Pointer Race Freedom
VMCAI
Polyhedral Approximation of Multivariate Polynomials using Handelman’s Theorem
VMCAI
Predicate Abstraction for Linked Data Structures
VMCAI
Program Analysis with Local Policy Iteration
VMCAI
Property Directed Abstract Interpretation
VMCAI
Regular Symmetry Patterns
VMCAI
Reward-Bounded Reachability Probability for Uncertain Weighted MDPs
VMCAI
Tight Cutoffs for Guarded Protocols with Fairness
VMCAI

Call for Papers

17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016) January 17-19, 2016, St. Petersburg, Florida, United States

https://conf.researchr.org/home/VMCAI-2016

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.

Scope

The program of VMCAI 2016 will consist of refereed research papers as well as invited lectures and tutorials. 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 Certification
  • Error Diagnosis
  • Program Transformation
  • Hybrid and Cyber-physical Systems

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

Important Dates

Event Date
Abstract submission Fri 4 Sep 2015
Paper submission Mon 14 Sep 2015 (extended)
Author notification Sat 10 Oct 2015
VMCAI 2016 conference Sun 17 - Tue 19 Jan 2016

Submissions

Submissions are restricted to 17 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.

Confirmed Invited Speakers

Student Travel Funding

The US National Science Foundation has provided funding to support student attendance at VMCAI 2016. Applicants must be registered students at accredited US academic institutions. Successful applicants will receive a grant to cover travel and other costs of attending VMCAI in St. Petersburg, Florida. Only students who are registered (or will register) for VMCAI, are eligible to apply.

If you are interested, please send the following information to vmcai2016@easychair.org:

  • Are you presenting a paper at VMCAI? If not, then a short paragraph on why you want to attend VMCAI.
  • An estimate of the cost (travel, registration, and accommodation).
  • A copy of your CV.

Program committee

Co-chairs, whom you can contact via vmcai2016@easychair.org:

  • Barbara Jobstmann (EPFL)
  • K. Rustan M. Leino (Microsoft Research)

Full details:

Call for Participation

17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)
17-19 January 2016, St. Petersburg, Florida, United States
Co-located with POPL 2016 (https://conf.researchr.org/home/POPL-2016)

https://conf.researchr.org/home/VMCAI-2016

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.

Invited talks:

  • Thomas Reps: Automating Abstract Interpretation
  • Bryan Parno: Ironclad - Full Verification of Complex Systems
  • Peter Müller: Viper - A Verification Infrastructure for Permission-based Reasoning

Important dates:

  • Student Travel Grant Application: 6 December 2015
  • Early registration: 18 December 2015
  • Conference: 17-19 January 2016

Registration (via the POPL 2016 registration site):

https://regmaster4.com/2016conf/POPL16/register.php

Accommodation (via POPL 2016 web site):

https://conf.researchr.org/venue/POPL-2016/key

Student Travel Grants:

The US National Science Foundation has provided funding to support student attendance at VMCAI 2016. Applicants must be registered students at an accredited US academic institution. Successful applicants will receive a grant to cover travel and other costs of attending VMCAI in St. Petersburg, Florida. Only students who are registered (or will register) for VMCAI, are eligible to apply.

If you are interested, please send the following information to vmcai2016@easychair.org:

  • Are you presenting a paper at VMCAI? If not, then a short paragraph on why you want to attend VMCAI.
  • An estimate of the cost (travel, registration, and accommodation).
  • A copy of your CV.

This document sets out the VMCAI policy on conflict of interest. All Program Committee chairs should read and be familiar with concepts in this document before the reviewing process begins.

Purpose of COI Rules

The conflict of interest rules are established to maintain the integrity of the peer review process. Their primary purposes are as follows:

  1. To maintain objectivity in reviewing. A reviewer with a personal connection to the author of a paper may feel that they can be objective in reviewing the paper. However, for the review process to be trusted, even the appearance of bias must be be avoided.

  2. To maintain confidentiality of the review process. Reviewers must be able to speak freely, unconstrained by any perceived personal connections of other reviewers to the authors. Again, it is the appearance of a conflict that is important here, since the appearance is sufficient to inhibit debate and discussion.

The second point is of great importance. If a PC member with a conflict of interest obtains access to a review of the paper in question, the confidentiality of the review process has been violated. This means that it is very important to discover conflicts before the review process begins.

Definition of Conflict of Interest

Generally, a PC member, chair or SC member has a conflict of interest with a submission if they would be reasonably perceived to personally benefit in some way by acceptance or rejection of the paper. This is a matter of judgment, but there are some specific situations in which a conflict clearly exists. These include people who are:

  1. An author of the submission.

  2. A collaborator with an author of the submission. You should consider yourself a collaborator if you have published a paper with the author or are currently working together on a project, or have applied for a grant together, or have worked together in a consulting relationship. Collaboration on the steering committee of a conference or editing a volume also counts (but an editor of a volume would not be considered in conflict with a contributor to that volume). A collaborator relationship is not permanent. Work occurring or published more than four years ago need not be considered a conflict.

  3. A person working at the same institution with an author of the submission. It is not always clear what constitutes an institution for this purpose. However, two people employed by the same university (even in different departments) or the same corporation, or the same government agency should be considered in conflict. Once the employment relationship ends, the conflict ends (so past employees of the same company are not usually considered in conflict).

  4. A person in a mentor relationship with a submission author, for example thesis advisor/advisee. This conflict is permanent, that is, you may never review a paper of your thesis advisors or past advisees. A post-doc, however, should be considered as an employee and collaborator, but not as an advisee.

  5. A person in conflict with an immediate family member of a submission author, or an immediate family member of a person in conflict. Generally, conflicts extend to family members because the interests of family members are perceived to be related.

Not all of these criteria are perfectly objective. In ambiguous cases** and in cases where deviation from the rules is deemed appropriate**, the PC chair(s) should use their judgment, keeping in mind the purposes of the COI rules as stated above: objectivity and confidentiality. If there is a reason why the person might appear to be not objective, or might appear to be connected to an author in a way that might inhibit free discussion, then there is a conflict.

Application of the COI Rules

Application of the COI rules is primarily by the PC members themselves. All PC members should be given a copy of this policy and asked to declare any known conflicts with submitted papers. In unclear cases, PC member should ask the PC chair(s) for guidance. The PC chairs should also, to the extent practical, make sure that obvious conflicts (for example, persons working at the same institution) are declared. The easychair system has a mechanism for declaring conflicts that prevents access to reviews and discussions by PC chairs and members with conflicts.

If a conflict is discovered after the review process has begun, the conflict should be immediately declared to the PC chairs either by the reviewer herself/himself or by any other PC member. All involved in the reviewing process of the paper should be notified, and the conflicted reviewer should have no further access to reviews or discussions. This must be done even if the result is that the number of reviews obtained is fewer than desired, and even if program committee discussion has already begun. If the case is not clear, the PC chairs may refer to the Steering Committee for a judgement (but of course, COI rules should be followed to ensure that SC members with conflicts are not included in the discussions).