Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online

Welcome to the website of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021).

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 2021 will be the 22nd edition in the series.

VMCAI will take place during January 17-19, 2021. The conference will be held as a virtual meeting due to the on going COVID-19 situation, employing

  • a single Zoom room for the presentation and interactive Q&A, with Zoom chat disabled, combined with

  • the POPL 2021 Clowdr server for chat functionality (e.g., asking questions during Q&A) and for breaks together with participants at concurrent POPL-colocated events.

The Zoom room is (only) reachable after logging into Clowdr. It will be open all VMCAI days (Sunday, Monday, Tuesday) from 15:00-20:00 CET (UTC+1) and can be used for socializing and informal chatting outside of the presentations sessions.

Clowdr login information will be provided to all registered participants directly from Clowdr (please check your spam folders).

Additional information and instructions on how to use Clowdr is available at How to POPL in 2021.

The sessions are streamed live on the YouTube channel VMCAI 2021.

Monday’s live stream can be found here.

Tuesday’s live stream can be found here.

Invited Talks

Dates
Plenary
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: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:30 - 16:00
15:30
30m
Social Event
Sunday Breakfast Tables
Workshops and Co-located Events

16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir Vizel Technion—Israel Institute of Technology
16:00
60m
Keynote
Model Checking Hyperproperties
VMCAI
I: Bernd Finkbeiner CISPA Helmholtz Center for Information Security
Media Attached
17:00 - 17:30
HyperpropertiesVMCAI at VMCAI
Chair(s): Grigory Fedyukovich Florida State University
17:00
15m
Talk
Compositional Model Checking for Multi-Properties
VMCAI
Ohad Goudsmid Department of Computer Science, The Technion, Orna Grumberg Technion – Israel Institute of Technology, Sarai Sheinvald Department of Software Engineering, ORT Braude College of Engineering
Media Attached
17:15
15m
Talk
Decomposing Data Structure Commutativity Proofs with mn-Differencing
VMCAI
Eric Koskinen Stevens Institute of Technology, Kshitij Bansal Google
Media Attached
17:30 - 18:00
17:30
30m
Break
Sunday Coffee Break
Workshops and Co-located Events

18:00 - 18:30
Infinite-State Systems and CompilationVMCAI at VMCAI
Chair(s): Orna Grumberg Technion – Israel Institute of Technology
18:00
15m
Talk
Proving the existence of fair paths in infinite state systems
VMCAI
Enrico Magnago Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler
Media Attached
18:15
15m
Talk
A Self-Certifying Compilation Framework for WebAssembly
VMCAI
Kedar Namjoshi Nokia Bell Labs, Anton Xue University of Pennsylvania
Media Attached
18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler Cohen Technion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina Peterson University of Central Florida, Victor Cook University of Central Florida, Damian Dechev University of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel Dietsch University of Freiburg, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Mehdi Naouar University of Freiburg, Andreas Podelski University of Freiburg, Germany, Claus Schätzle University of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Informal Systems Inc, Josef Widder Informal Systems, Florian Zuleger Vienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie Bertrand INRIA Rennes, Marijana Lazic Technical University of Munich, Josef Widder Informal Systems
Media Attached
19:30 - 20:00
19:30
30m
Social Event
Sunday Hallway Time
Workshops and Co-located Events

Mon 18 Jan

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

15:30 - 16:00
15:30
30m
Social Event
Topic Oriented Discussions
Workshops and Co-located Events

16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir Vizel Technion—Israel Institute of Technology
16:00
60m
Keynote
Algebra-based Synthesis of Loops and their Invariants
VMCAI
I: Laura Kovacs Vienna University of Technology (TU Wien), Andreas Humenberger Vienna University of Technology
Media Attached
17:00 - 17:30
Abstract InterpretationVMCAI at VMCAI
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
17:00
15m
Talk
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
VMCAI
Franck Védrine CEA LIST, Maxime Jacquemin CEA LIST, France, Nikolai Kosmatov Thales Research and Technology, Julien Signoles CEA LIST
Media Attached
17:15
15m
Talk
Twinning automata and regular expressions for string static analysis
VMCAI
Luca Negrini Ca’ Foscari University of Venice, Julia S.r.l., Vincenzo Arceri Ca’ Foscari University of Venice, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia
Media Attached
17:30 - 18:00
17:30
30m
Break
Monday Coffee Break 2
Workshops and Co-located Events

18:00 - 18:30
Model CheckingVMCAI at VMCAI
Chair(s): James R. Wilcox University of Washington
18:00
15m
Talk
Unbounded Procedure Summaries from Bounded Environments
VMCAI
Lauren Pick Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University
Media Attached
18:15
15m
Talk
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
VMCAI
Hongce Zhang Princeton University, Aarti Gupta Princeton University, Sharad Malik Princeton University
Media Attached
18:30 - 19:15
Synthesis and RepairVMCAI at VMCAI
Chair(s): Aws Albarghouthi University of Wisconsin-Madison, USA
18:30
15m
Talk
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
VMCAI
Marius Kamp Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Friedrich-Alexander University Erlangen-Nürnberg (FAU)
Media Attached
18:45
15m
Talk
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
VMCAI
Thanh-Toan Nguyen National University of Singapore, Quang-Trung Ta National University of Singapore, Ilya Sergey Yale-NUS College and National University of Singapore, Wei-Ngan Chin National University of Singapore
Media Attached
19:00
15m
Talk
GPURepair: Automated Repair of GPU Kernels
VMCAI
Saurabh Joshi IIT Hyderabad, Gautam Muduganti IIT Hyderabad
Media Attached
19:30 - 20:00
19:30
30m
Social Event
Monday Shuffle-Space Time
Workshops and Co-located Events

Tue 19 Jan

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

15:30 - 16:00
15:30
30m
Social Event
Tuesday Shuffle-Space Time
Workshops and Co-located Events

16:00 - 17:00
Invited talkVMCAI at VMCAI
16:00
60m
Keynote
Generative Program Analysis and Beyond: The Power of Domain-Specific Languages
VMCAI
I: Bernhard Steffen TU Dortmund, Alnis Murtovi TU Dortmund, David Schmidt Kansas State University
Media Attached
17:00 - 17:30
ApplicationsVMCAI at VMCAI
Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security
17:00
15m
Talk
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
VMCAI
Yahui Song National University of Singapore, Wei-Ngan Chin National University of Singapore
Media Attached
17:15
15m
Talk
A Design of GPU-Based Quantitative Model Checking
VMCAI
YoungMin Kwon SUNY Korea, Eunhee Kim 2e Consulting Corp.
Media Attached
17:30 - 18:00
17:30
30m
Break
Tuesday Coffee Break 2
Workshops and Co-located Events

18:00 - 18:30
Case StudiesVMCAI at VMCAI
Chair(s): Roderick Bloem Institute of Software Technology, Graz University of Technology
18:00
15m
Talk
Formal Semantics and Verification of Network Based Biocomputation Circuits
VMCAI
Michelle Aluf-Medina Bar Ilan University, Till Korten TU Dresden, Avraham Raviv Bar Ilan University, Dan Nicolau Jr. Molecular Sense, Hillel Kugler Bar Ilan University
Media Attached
18:15
15m
Talk
Netter: Probabilistic, Stateful Network Models
VMCAI
Han Zhang Carnegie Mellon University, Chi Zhang CMU, Arthur Azevedo de Amorim Carnegie Mellon University, USA, Yuvraj Agarwal Carnegie Mellon University, Matt Fredrikson Carnegie Mellon University, Limin Jia Carnegie Mellon University
Media Attached
18:30 - 19:30
Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. Summers University of British Columbia
18:30
15m
Talk
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
VMCAI
Martin Bromberger MPI-INF, Alberto Fiori Max Planck Institute for Informatics, Christoph Weidenbach MPI-INF
Media Attached
18:45
15m
Talk
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Jochen Hoenicke University of Freiburg, Tanja Schindler University of Freiburg
Media Attached
19:00
15m
Talk
On Pre- and Inprocessing for Weighted MaxSAT
VMCAI
Tobias Paxian University of Freiburg, Pascal Raiola University of Freiburg, Bernd Becker Albert-Ludwigs-University Freiburg
Media Attached
19:15
15m
Talk
Compositional Satisfiability Solving in Separation Logic
VMCAI
Quang Loc Le University College London, UK
Media Attached
19:30 - 20:00
19:30
30m
Break
Welcome to Copenhagen!
Workshops and Co-located Events

Accepted Papers

Title
A Design of GPU-Based Quantitative Model Checking
VMCAI
Media Attached
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
VMCAI
Media Attached
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Media Attached
A Self-Certifying Compilation Framework for WebAssembly
VMCAI
Media Attached
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
VMCAI
Media Attached
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
VMCAI
Media Attached
Compositional Model Checking for Multi-Properties
VMCAI
Media Attached
Compositional Satisfiability Solving in Separation Logic
VMCAI
Media Attached
Concurrent Correctness in Vector Space
VMCAI
Media Attached
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
VMCAI
Media Attached
Decomposing Data Structure Commutativity Proofs with mn-Differencing
VMCAI
Media Attached
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Media Attached
Formal Semantics and Verification of Network Based Biocomputation Circuits
VMCAI
Media Attached
GPURepair: Automated Repair of GPU Kernels
VMCAI
Media Attached
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Media Attached
Netter: Probabilistic, Stateful Network Models
VMCAI
Media Attached
On Pre- and Inprocessing for Weighted MaxSAT
VMCAI
Media Attached
Proving the existence of fair paths in infinite state systems
VMCAI
Media Attached
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
VMCAI
Media Attached
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
VMCAI
Media Attached
Twinning automata and regular expressions for string static analysis
VMCAI
Media Attached
Unbounded Procedure Summaries from Bounded Environments
VMCAI
Media Attached
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Media Attached

Call for Artifacts

VMCAI 2021 continues 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.

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

Artifact submission is optional. However, we highly encourage all authors to also submit an artifact. A successfully evaluated artifact can increase your chance of being accepted since the evaluation result of your artifact is taken into account during paper reviewing. Additionally, badges shown on the title page of the corresponding paper give you credit for good artifact submissions.

We award two types of badges that are granted independently of each other. For artifacts that are successfully evaluated by the artifact evaluation committee we grant the replicated badge. Artifacts that are publically available under a DOI receive an availability badge. Authors may use all granted badges on the title page of the respective paper.

Important Dates

The artifact evaluation will be done in parallel with the submission. The artifacts are submitted less than 1 week after the paper submission.

What When
Artifact registration (abstract submission) 13th Oct 2020
Artifact submission 15th Oct 2020
Artifact test phase notification 19th Oct 2020
Artifact clarification period 19th-22th Oct 2020
Artifact notification 10th Nov 2020

All artifacts are evaluated by the artifact evaluation committee. Each artifact will be reviewed by at least two committee members. 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.

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

  • 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

An artifact submission should consist of

  • an abstract that summarizes the artifact and explains its relation to the paper including

  • a URL from which a .zip or .tar.gz archive file containing the artifact can be downloaded - we encourage you to provide a DOI - and

  • the SHA256 checksum of the archive file, and

  • a .pdf file of the submitted paper.

The artifact evaluation chairs will download the archive file and distribute it to the reviewers. Please also look at the Artifact Packaging Guidelines section for detailed information about the contents of the submission.

The abstract including the URL of the download link, as well as the SHA256 checksum of your archive file, and the .pdf file of your paper must be submitted to EasyChair.

https://easychair.org/conferences/?conf=vmcai2021ae

We need the checksum to ensure the integrity of your artifact. You can generate the checksum using the following command-line tools.

  • Linux: sha256sum <file>
  • Windows: CertUtil -hashfile <file> SHA256
  • MacOS: shasum -a 256 <file>

If you cannot submit the artifact as requested or encounter any other difficulties in the submission process, please contact the artifact evaluation chairs prior to submission.

Artifact Packaging Guidelines

We expect that authors package their artifact (archive file) and write their instructions such that the artifact evaluation committee can evaluate the artifact within a virtual machine provided by us. Only submit the required files to replicate your results in the provided virtual machine. Do not submit a virtual machine image in the archive file. AEC members will copy your archive file into the provided virtual machine.

We recommend prearing your artifact in such a way that any computer science expert without dedicated expertise in your field can use your artifact, especially to replicate your results. For example, provide easy-to-use scripts and a detailed README document.

VMCAI 2021 Virtual Machine

An initial version of the virtual machine is now available from https://zenodo.org/record/4017293

See the linked page for more information on how to use it.

In case you think the VM is improper for evaluation of your artifact, please contact the artifact evaluation chairs prior to artifact submission.

Submission Contents

Your artifact archive file must contain the following elements.

  1. The main artifact, i.e., data, software, libraries, scripts, etc. required to replicate the results of your paper. ◦ The review will be singly blind. Please make sure that you do not (accidentally) learn the identify of the reviewers (e.g., through analytics, logging).

  2. A license file. Your license needs to allow the artifact evaluation chairs to download and distribute the artifact to the artifact evaluation committee members and the artifact evaluation committee members must be allowed to evaluate the artifact, e.g., use, execute, and modify the artifact for the purpose of artifact evaluation.

  3. A README text file that introduces the artifact to the user and guides the user through replication of your results. Ideally, it should consist of the following parts:

  • We describing the structure and content of your artifact.

  • It should describe the steps to set up your artifact within the provided VM. To simplify the reviewing process, we recommend to provide an installation script (if necessary).

  • We would appreciate it if you would support the reviewers not only for the main review phase but also for the testing phase. To this end, it would be helpful if you would provide instructions that allow installation and rudimentary testing (i.e., in such a way that technical difficulties would pop up) in as little time as possible.

  • Document in detail how to replicate your results of the paper:

    • Please document which claims or results of the paper can be replicated with the artifact and how (e.g., which experiment must be performed). Please also explain which claims and results cannot be replicated and why.

    • Describe in detail how to replicate the results in the paper, especially describe the steps that need to be performed to replicate the results in the paper. To simplify the reviewing process, we recommend to provide evaluation scripts (where applicable).

    • Precisely state the resource requirements (RAM, number of cores, CPU frequency, etc.), which you used to test your artifact. Your resource requirements should be modest and allow replication of results even on laptops.

    • Please provide for each task/step of the replication (an estimate) how long it will take to perform it or how long it took for you and what exact machine(s) you used.

    • For tasks that require a large amount of resources (hardware or time), we recommend to provide a possibility to replicate a subset of the results with reasonably modest resource and time limits, e.g., within 8 hours on a reasonable personal computer. In this case, please also include a script to replicate only a subset of the results. If this is not possible, please contact the artifact evaluation chairs early, but no latter than before submission.

Publication of Artifacts

The artifact evaluation committee uses the submitted artifact only for the artifact evaluation. It may not publicize the artifact or any parts of it during or after completing evaluation. Artifacts and all associated data will be deleted at the end of the evaluation process. We encourage the authors of artifacts to make their artifacts also permanently available, e.g., on ZENODO or figshare.com, and refer to them in their papers via a DOI. All artifacts for which a DOI exists that is known to the artifact evaluation committee are granted the availability badge.

Badges

Our badges were kindly provided by Claus Schätzle and are licensed under CC0. They are also available from GitHub. You will receive a mail from the artifact evaluation chairs detailing which badges you can use.

Call for Papers

VMCAI 2021 is the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation. The conference will be held on January 17-19, 2021, in Copenhagen, Denmark, as a physical, virtual, or hybrid physical/virtual meeting depending on the COVID-19 situation. 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 2021 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 and distributed Systems
  • Analysis of numerical properties
  • Analysis of smart contracts
  • Analysis of neural networks
  • Case Studies on all of the above topics Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, and object-oriented programming.

Important Dates AoE (UTC-12)

October 5th, 2020 October 11th, 2020 Paper submission

November 6th, 2020 November 10th, 2020 Notification

November 13th, 2020 November 16th, 2020 Camera-ready

Conference Submission Link

https://easychair.org/conferences/?conf=vmcai2021

Submissions

Submissions are required to follow Springer’s LNCS format. The page limit depends on the paper’s category (see below). In each category, additional material beyond the page limit may be placed in a clearly marked 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

Submissions will undergo a single-blind review process. Accepted papers will be published in Springer’s Lecture Notes in Computer Science series. There will be three categories of papers: regular papers, tool papers and case studies. Papers in each category have a different page limit and will be evaluated differently.

Regular papers clearly identify and justify an advance to the field of verification, abstract interpretation, or model checking. Where applicable, they are supported by experimental validation. Regular papers are restricted to 20 pages in LNCS format, not counting references.

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 an artifact. Tool papers are restricted to 12 pages in LNCS format, not counting references.

Case studies are expected to describe the use of verification, model checking, and abstract interpretation techniques in new application domains or industrial settings. Papers in this category do not necessarily need to present original research results but are expected to contain novel applications of formal methods techniques as well as an evaluation of these techniques in the chosen application domain. Such papers are encouraged to discuss the unique challenges of transferring research ideas to a real-world setting and reflect on any lessons learned from this technology transfer experience. Case study papers are restricted to 20 pages in LNCS format, not counting references. (Shorter case study papers are also welcome.)

Artifacts

VMCAI 2021 allows authors 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 will be available on the conference webpage: https://popl21.sigplan.org/home/VMCAI-2021

Organizing Committee

Fritz Henglein - University of Copenhagen, Denmark

Sharon Shoham - Tel Aviv University, Israel

Yakir Vizel - The Technion, Israel

Registration for VMCAI 2021 is through POPL’s registration web-page, as part of POPL’s co-events, and provides a choice between a full (regular/student) registration fee or a discounted fee. There are no restrictions/requirements for choosing the discounted fee option.

Early registration closes on January 10th.

The proceedings can be found here: VMCAI 2021 on Springer