Write a Blog >>

Welcome to the website of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2020).

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 2020 will be the 21st edition in the series.

Supporters

Call for Papers

21th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2020) January 19-21 2020, New Orleans, Louisiana, United States.

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

Important Dates

Submission 1st Oct 2019
Notification 7th Nov 2019
Camera-ready 15th Nov 2019
Conference 19th to 21st Jan 2020

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.

Submission link: https://easychair.org/conferences/?conf=vmcai2020

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

There will be two categories of papers: regular and tool papers. Both types of paper have the same format but will be evaluated differently.

  • Regular paper clearly identify and justify a advance to the field of verification, abstract interpretation, or model checking. Where applicable, they are supported by experimental validation.
  • Tool papers present a new tool, a new tool component, or novel extensions to an existing tool. They should provide a short description of the theoretical foundations with relevant citations, and emphasize the design and implementation concerns, including software architecture and core data structures. A regular tool paper should give a clear account of the tool’s functionality, discuss the tool’s practical capabilities with reference to the type and size of problems it can handle, describe experience with realistic case studies, and where applicable, provide a rigorous experimental evaluation. Papers that present extensions to existing tools should clearly focus on the improvements or extensions with respect to previously published versions of the tool, preferably substantiated by data on enhancements in terms of resources and capabilities. Authors are strongly encouraged to make their tools publicly available and submit and artifact.

Artifacts

VMCAI 2020 is introducing the possibility to submit an artifact along a paper. Artifacts are any additional material that substantiates the claims made in the paper, and ideally makes them fully replicable. Submitting an artifact is encouraged but not required. The artifact will be evaluated in parallel with the submission by the artifact evaluation committee (AEC). The AEC will read the paper and evaluate the artifact on the following criteria:

  • consistency with and replicability of results in the paper,
  • completeness,
  • documentation, and
  • ease of use.

More information can be found on the artifact webpage: Call for Artifacts

Call for Artifacts

VMCAI 2020 is introducing the possibility to submit an artifact along a paper. Artifacts are any additional material that substantiates the claims made in the paper, and ideally makes them fully replicable. For some papers, these artifacts are as important as the paper itself because they provide crucial evidence for the quality of the results.

The goal of artifact evaluation is twofold. On the one hand, we want to encourage authors to provide more substantial evidence to their papers and to reward authors who create artifacts. On the other hand, we want to simplify the independent replication of results presented in the paper and to ease future comparison with existing approaches. Artifact submission is optional.

Artifacts of interest include (but are not limited to):

  • Software, Tools, or Frameworks
  • Data sets
  • Test suites
  • Machine checkable proofs
  • Any combination of them
  • Any other artifact described in the paper

Important Dates

The artifact evaluation will be done in parallel with the submission. The artifact are submitted at most 1 week after the paper submission.

Artifact submission 8th Oct 2019
Artifact test phase notification 15th Oct 2019
Artifact clarification period 15th-18th Nov 2019

Artifact Evaluation

All artifacts are evaluated by the artifact evaluation committee. Reviewers will read the paper and explore the artifact to evaluate how well the artifact supports the claims and results of the paper. The evaluation is based on the following questions.

  • Is the artifact consistent with the paper and the claims made by the paper?
  • Are the results of the paper replicable through the artifact?
  • Is the artifact complete, i.e., how many of the results of the paper are replicable?
  • Is the artifact well-documented?
  • Is the artifact easy to use?

The artifact evaluation is performed in the following two phases.

  1. In the test phase, reviewers check if the artifact is functional, i.e., they look for setup problems (e.g., corrupted, missing files, crashes on simple examples, etc.). If any problems are detected, the authors are informed of the outcome and asked for clarification. The authors will get 3 days to respond to the reviews in case problems are encountered.
  2. In the assessment phase, reviewers will try to reproduce any experiments or activities and evaluate the artifact w.r.t the questions detailed above.

Artifacts Submission

The details for the submission will be available soon.

VMCAI Winter School is a winter school on formal methods associated with VMCAI 2020 that will take place in New Orleans, Louisiana on January 16-18, 2019. In the vein of VMCAI, the school is meant to facilitate interaction, cross-fertilization, and advancement of hybrid methods that combine Software Verification, Program Analysis, and Model Checking.

The school will cover several fundamental aspects of formal methods and applications.

Program

TBA

Registration

The VMCAI Winter School will be free but registration is required.

Travel and Accommodation Support

PhD students can apply for a grant covering to cover travel to the winter school and accommodation during the winter school. Information about the application procedure will be available soon.

Questions? Use the VMCAI contact form.