Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017

18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)

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

Sun 15 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 1VMCAI at Amphitheater 44
Chair(s): David Monniaux CNRS, VERIMAG
09:00
60m
Talk
Detecting Strict Aliasing Violations in the Wild
VMCAI
Pascal Cuoq Trust-in-Soft
File Attached
10:30 - 12:00
Program AnalysisVMCAI at Amphitheater 44
Chair(s): Boris Yakobowski CEA - LIST
10:30
30m
Talk
Partitioned Memory Models for Program Analysis.
VMCAI
Wei Wang Google, Inc., Clark Barrett Stanford University, Thomas Wies New York University
File Attached
11:00
30m
Talk
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
VMCAI
Asya Frumkin Tel Aviv University, Yotam M. Y. Feldman Tel Aviv University, Ondřej Lhoták University of Waterloo, Canada, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
File Attached
11:30
30m
Talk
Stabilizing Floating-Point Programs using Provenance Analysis
VMCAI
Yijia Gu Northeastern University, Thomas Wahl Northeastern University
14:00 - 15:30
Concurrency 1VMCAI at Amphitheater 44
Chair(s): Camille Coti LIPN, Université Paris 13
14:00
30m
Talk
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
VMCAI
14:30
30m
Talk
Independence Abstractions and Models of Concurrency
VMCAI
Vijay D'Silva Google Inc., Daniel Kroening University of Oxford, Marcelo Sousa University of Oxford
15:00
30m
Talk
Static Analysis of Communicating Process using Symbolic Transducers
VMCAI
Vincent Botbol CEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le Gall CEA LIST, Emmanuel Chailloux LIP6 - UPMC
Media Attached File Attached
16:00 - 17:30
Decision proceduresVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
16:00
30m
Talk
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
VMCAI
Ernst Moritz Hahn State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
File Attached
16:30
30m
Talk
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
VMCAI
Andrew Reynolds EPFL, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Cristina Serban VERIMAG, CNRS, Université Grenoble-Alpes
File Attached
17:00
30m
Talk
Matching multiplications in Bit-Vector formulas
VMCAI
Supratik Chakraborty IIT Bombay, Ashutosh Gupta , Rahul Jain Tata Institute of Fundamental Research
File Attached

Mon 16 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 2VMCAI at Amphitheater 44
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
09:00
60m
Talk
Verified Concurrent Code: Tricks of the Trade
VMCAI
A: Ernie Cohen Amazon Web Services
10:30 - 12:00
Numerical domainsVMCAI at Amphitheater 44
Chair(s): Laure Gonnord University of Lyon & LIP, France
10:30
30m
Talk
Sound Bit-Precise Numerical Domains
VMCAI
Tushar Sharma University of Wisconsin - Madison, USA, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
File Attached
11:00
30m
Talk
Efficient Elimination of Redundancies in Polyhedra using Raytracing
VMCAI
Media Attached File Attached
11:30
30m
Talk
Finding Relevant Templates via the Principal Component Analysis
VMCAI
Yassamine Seladji University of Tlemcen
File Attached
14:00 - 15:30
Model-checking and bug findingVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
14:00
30m
Talk
Effective Bug Finding in C Programs with Shape and Effect Abstraction
VMCAI
Iago Abal IT University of Copenhagen, Claus Brabrand IT University of Copenhagen, Denmark, Andrzej Wąsowski IT University of Copenhagen, Denmark
14:30
30m
Talk
Reduction of Workflow Nets for Generalised Soundness Verification
VMCAI
Hadrien Bride Femto-ST / Université de Franche-Comté, Olga Kouchnarenko Femto-ST / Université de Franche-Comté, Fabien Peureux Femto-ST / Université de Franche-Comté + Smartesting S&S
Media Attached
15:00
30m
Talk
Dynamic Reductions for Model Checking Concurrent Software.
VMCAI
Henning Günther Technische Universität Wien, Alfons Laarman Vienna University of Technology, Ana Sokolova University of Salzburg, Georg Weissenbacher Technische Universität Wien
File Attached
16:00 - 17:30
Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44
Chair(s): Constantin Enea LIAFA, Université Paris Diderot
16:00
30m
Talk
Block-wise abstract interpretation by combining abstract domains with SMT
VMCAI
16:30
30m
Talk
IC3 - Flipping the E in ICE
VMCAI
Yakir Vizel , Arie Gurfinkel University of Waterloo, Sharon Shoham Tel Aviv university, Sharad Malik Princeton University
17:00
30m
Talk
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
VMCAI
Lukáš Holík , Martin Hruska Brno University of Technology , Ondřej Lengál Brno University of Technology , Adam Rogalewicz Brno University of Technology , Tomáš Vojnar Brno University of Technology
19:30 - 22:00
BanquetVMCAI at Procope

Tue 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 3VMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
09:00
60m
Talk
Verification of Cancer Programs
VMCAI
Jasmin Fisher Microsoft Research
10:30 - 12:00
Model Checking and SynthesisVMCAI at Amphitheater 44
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
10:30
30m
Talk
Reachability for dynamic parametric processes
VMCAI
Anca Muscholl Université de Bordeaux / LaBRI, Helmut Seidl Technische Universität München, Igor Walukiewicz CNRS, LaBRI
11:00
30m
Talk
Synthesizing Non-Vacuous Systems
VMCAI
Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler , ma e , Ofer Strichman Technion
File Attached
11:30
30m
Talk
Solving Nonlinear Integer Arithmetic with MCSat
VMCAI
Dejan Jovanović SRI International
14:00 - 15:30
Abstract InterpretationVMCAI at Amphitheater 44
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:00
30m
Talk
Complete Abstractions and Subclassical Modal Logics
VMCAI
Vijay D'Silva Google, Marcelo Sousa University of Oxford
14:30
30m
Talk
Structuring Abstract Interpreters through State and Value Abstractions
VMCAI
David Bühler CEA LIST, Boris Yakobowski CEA - LIST, Sandrine Blazy University of Rennes 1, France
Media Attached
15:00
30m
Talk
Conjunctive Abstract Interpretation using Paramodulation
VMCAI
Mooly Sagiv Tel Aviv University, A: Or Ozeri Tel Aviv university, Oded Padon Tel Aviv University, Noam Rinetzky Tel Aviv University
Media Attached
16:00 - 17:30
Concurrency 2VMCAI at Amphitheater 44
Chair(s): David Monniaux CNRS, VERIMAG
16:00
30m
Talk
Using Abstract Interpretation to Correct Synchronization Faults
VMCAI
Pietro Ferrara IBM Research, Omer Tripp IBM Thomas J. Watson Research Center, Peng Liu Purdue University, Eric Koskinen Yale University
16:30
30m
Talk
Detecting All High-Level Dataraces in an RTOS Kernel.
VMCAI
Suvam Mukherjee Indian Institute of Science, Arunkumar S Indian Institute of Science, Deepak D'Souza
17:00
30m
Talk
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
VMCAI
Raphaël Monat Ecole Normale Supérieure de Lyon, Antoine Miné UPMC, France

Call For Papers

Title
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
VMCAI
Block-wise abstract interpretation by combining abstract domains with SMT
VMCAI
Complete Abstractions and Subclassical Modal Logics
VMCAI
Conjunctive Abstract Interpretation using Paramodulation
VMCAI
Media Attached
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
VMCAI
Detecting All High-Level Dataraces in an RTOS Kernel.
VMCAI
Detecting Strict Aliasing Violations in the Wild
VMCAI
File Attached
Dynamic Reductions for Model Checking Concurrent Software.
VMCAI
File Attached
Effective Bug Finding in C Programs with Shape and Effect Abstraction
VMCAI
Efficient Elimination of Redundancies in Polyhedra using Raytracing
VMCAI
Media Attached File Attached
Finding Relevant Templates via the Principal Component Analysis
VMCAI
File Attached
IC3 - Flipping the E in ICE
VMCAI
Independence Abstractions and Models of Concurrency
VMCAI
Matching multiplications in Bit-Vector formulas
VMCAI
File Attached
Partitioned Memory Models for Program Analysis.
VMCAI
File Attached
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
VMCAI
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
VMCAI
File Attached
Reachability for dynamic parametric processes
VMCAI
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
VMCAI
File Attached
Reduction of Workflow Nets for Generalised Soundness Verification
VMCAI
Media Attached
Solving Nonlinear Integer Arithmetic with MCSat
VMCAI
Sound Bit-Precise Numerical Domains
VMCAI
File Attached
Stabilizing Floating-Point Programs using Provenance Analysis
VMCAI
Static Analysis of Communicating Process using Symbolic Transducers
VMCAI
Media Attached File Attached
Structuring Abstract Interpreters through State and Value Abstractions
VMCAI
Media Attached
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
VMCAI
File Attached
Synthesizing Non-Vacuous Systems
VMCAI
File Attached
Using Abstract Interpretation to Correct Synchronization Faults
VMCAI
Verification of Cancer Programs
VMCAI
Verified Concurrent Code: Tricks of the Trade
VMCAI

Call for Papers

18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017) January 15-17 2017, Paris, France

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

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

  • Abstract submission Extended to Sept 25, 2016 AOE
  • Paper submission Extended to Sept 28, 2016 AOE
  • Author notification Nov 14, 2016
  • Final Version Nov 28 , 2016
  • VMCAI 2017 conference January 15-17 2017, Paris, France

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.

Invited Speakers

Program Committee

Co-chairs, whom you can contact via vmcai2017@easychair.org: Ahmed Bouajjani and David Monniaux

Call For Participation

International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI 2017 Paris, January 15-17, 2017 https://conf.researchr.org/home/VMCAI-2017

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 2017 will be the 18th edition in the series. The program of the conference includes 3 invited talks and 27 presentations of selected contributions.

VMCAI’17 is co-located with the international conference POPL’17, and it will take place in the Paris Jussieu Campus.

INVITED SPEAKERS:

  • Pascal Cuoq (Trust-in-Soft)
  • Ernie Cohen (Amazon Web Services)
  • Jasmin Fisher (Microsoft Research)

REGISTRATION:

Registrations are open: https://conf.researchr.org/attending/VMCAI-2017/registration NB: early registrations are until Dec 17, 2016.

SUPPORT FOR STUDENTS:

PhD students can apply for a grant covering their registrations fees. We encourage particularly female students to apply for this grant. Due to budget restrictions, a limited number of students can benefit from this support. Interested students must apply before Dec 9, 2016, 23:59 AoE, by sending a request to abou@irif.fr and David.Monniaux@imag.fr mentioning their name, affiliation, and contact information (address, email). Applicants will be notified by Dec 13, 2016.

PROGRAM

https://conf.researchr.org/track/VMCAI-2017/VMCAI-2017-papers#program

Igor Konnov, Josef Widder, Francesco Spegni and Luca Spalazzi. Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Roderick Bloem, Hana Chockler, Masoud Ebrahimi and Ofer Strichman. Synthesizing Non-Vacuous Systems
Iago Abal, Claus Brabrand and Andrzej Wasowski. Effective Bug Finding in C Programs with Shape and Effect Abstractions
Ernst Moritz Hahn, Sven Schewe, Andrea Turrini and Lijun Zhang. Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
Andrew Reynolds, Radu Iosif and Cristina Serban. Reasoning in the Bernays-Schonfinkel-Ramsey Fragment of Separation Logic
Anca Muscholl, Helmut Seidl and Igor Walukiewicz. Reachability for dynamic parametric processes
Tushar Sharma and Thomas Reps. Sound Bit-Precise Numerical Domains
Raphaël Monat and Antoine Miné. Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
Alexandre Maréchal and Michael Perin. Efficient Elimination of Redundancies in Polyhedra using Raytracing
Hadrien Bride, Olga Kouchnarenko and Fabien Peureux. Reduction of Workflow Nets for Generalised Soundness Verification
Supratik Chakraborty, Ashutosh Gupta and Rahul Jain. Matching multiplications in Bit-Vector formulas
Henning Günther, Alfons Laarman, Ana Sokolova and Georg Weissenbacher. Dynamic Reductions for Model Checking Concurrent Software
Pietro Ferrara, Omer Tripp, Peng Liu and Eric Koskinen. Using Abstract Interpretation to Correct Synchronization Faults
Or Ozeri, Oded Padon, Noam Rinetzky and Mooly Sagiv. Conjunctive Abstract Interpretation using Paramodulation
Yassamine Seladji. Finding Relevant Templates via the Principal Component Analysis
Wei Wang, Clark Barrett and Thomas Wies. Partitioned Memory Models for Program Analysis
Vincent Botbol, Tristan Le Gall and Emmanuel Chailloux. Static Analysis of Communicating Process using Symbolic Transducers
Asya Frumkin, Yotam M. Y. Feldman, Ondřej Lhoták, Oded Padon, Mooly Sagiv and Sharon Shoham. Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Yijia Gu and Thomas Wahl. Stabilizing Floating-Point Programs using Provenance Analysis
Dejan Jovanović. Solving Nonlinear Integer Arithmetic with MCSat
Vijay D'Silva, Daniel Kroening and Marcelo Sousa. Independence Abstractions and Models of Concurrency
Vijay D'Silva and Marcelo Sousa. Complete Abstractions and Subclassical Modal Logics
Yakir Vizel, Arie Gurfinkel, Sharon Shoham and Sharad Malik. IC3 - Flipping the E in ICE
Suvam Mukherjee, Arunkumar S and Deepak Dsouza. Detecting All High-Level Dataraces in an RTOS Kernel
Jiahong Jiang, Liqian Chen, Xueguang Wu and Ji Wang. Block-wise abstract interpretation by combining abstract domains with SMT
Lukas Holik, Martin Hruska, Ondrej Lengal, Adam Rogalewicz and Tomas Vojnar. Counterexample Validation and Interpolation-Based Refinement for Forest Automata
David Bühler, Boris Yakobowski and Sandrine Blazy. Structuring Abstract Interpreters through State and Value Abstractions

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:

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.

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:

An author of the submission.

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.

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).

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.

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).

  • Pascal Cuoq (Trust-in-Soft)
  • Ernie Cohen (Amazon Web Services)
  • Jasmin Fisher (Microsoft Research)