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 2026 will be the 27th edition in the series.

VMCAI 2026 will take place during January 12-13, 2026 as a physical (in-person) event in Rennes, France, co-located with POPL 2026. For each accepted paper, at least one author is required to register for the conference and present the paper in person.

Website: https://conf.researchr.org/home/VMCAI-2026

Important Dates
===============
Submission deadline: 10th September 2025
Notification: 6th November 2025
Camera-ready version due: 20th November 2025

List of Topics
==============
The program will consist of refereed research papers as well as invited talks. 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
verification for quantum computation
analysis of numerical properties
analysis of smart contracts
analysis of neural networks
case studies on all of the above topics

Submission Guidelines
=====================
Submissions are required to follow Springer’s LNCS format. The page limit depends on the paper’s category (see below). Submission is done via EasyChair at https://easychair.org/my/conference?conf=vmcai2026.

Submissions will undergo a single-blind review process. VMCAI 2026 accepts paper submissions in three categories: regular papers, tool papers, and case studies. Papers in each category have a different page limit and will be evaluated differently.

All accepted papers will be published in Springer’s Lecture Notes in Computer Science series. The corresponding author of each paper will need to complete and sign a License-to-Publish form to be submitted together with the camera-ready version.

**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 should contain original research and sufficient detail to assess the merits and relevance of the contribution, and will be evaluated on the basis of a combination of correctness, technical depth, significance, novelty, clarity, and elegance. 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.)

Authors can include a clearly marked appendix at the end of their submissions that is exempt from the page limit restrictions. However, the reviewers are not obliged to read the contents of these appendices. Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed

Call for Artifacts
==================
VMCAI 2026 makes available the option to submit an artifact along with a paper. Artifacts are any additional material that substantiates the claims made in the paper, and ideally makes them fully replicable.

PC Chairs
========
Yu-Fang Chen (Academia Sinica, Taiwan)
Thomas Jensen (INRIA, France)
Ondřej Lengál (Brno University of Technology, Czech Republic)

Artifact Evaluation Chairs
====================
Marek Chalupa (ISTA, Austria)
Yong Li (Chinese Academy of Sciences, China)

Program Committee
================
Alexander Bakst (Certora)
Sebastien Bardin (CEA LIST)
Borzoo Bonakdarpour(Michigan State University)
Filip Cano (Institute of Science and Technology Austria)
Milan Ceska (Faculty of Information Technology, Brno University of Technology)
Liqian Chen (National University of Defense Technology)
Chih-Hong Cheng (Chalmers University of Technology)
Coen De Roover (Vrije Universiteit Brussel)
Gidon Ernst (Ludwig Maximilian University of Munich)
Javier Esparza (Technical University of Munich)
Grigory Fedyukovich (Florida State University)
Vijay Ganesh (Georgia Tech)
Roberto Giacobazzi (University of Arizona, Department of Computer Science)
Simon Guilloud (Swiss Institute of Technology Lausanne)
Ashutosh Gupta (TIFR)
Lukáš Holík (Brno University of Technology)
Chih-Duo Hong (National Chengchi University)
Sebastian Junges (Radboud University)
Jan Kofroň (Charles University)
Alfons Laarman (Leiden University)
Nian-Ze Lee (National Taiwan University)
Matthieu Lemerre (CEA LIST)
Jérôme Leroux (CNRS)
Jyun-Ao Lin (National Taipei University of Technology)
Isabella Mastroeni (Universita' di Verona - Dipartimento di Informatica)
Nicolas Mazzocchi (Slovak University of Technology in Bratislava)
Antoine Miné (LIP6, UPMC)
Alexandre Moine (New York University)
Benoît Montagu (INRIA)
Jorge A Navas (Certora)
Luca Negrini (Ca' Foscari University of Venice)
Jakob Piribauer (TU Dresden)
Francesco Ranzato (University of Padova)
Christoph Scholl (University of Freiburg)
Stephen F. Siegel (University of Delaware)
Mihaela Sighireanu (Université Paris-Saclay, CNRS, ENS Paris-Saclay)
Julien Signoles (CEA LIST)
B Srivathsan (Chennai Mathematical Institute)
Marielle Stoelinga (University of Twente)
Jan Strejček (Masaryk University)
Kohei Suenaga (Kyoto University)
Tom van Dijk (University of Twente)
Masaki Waga (Kyoto University)
Kazuki Watanabe (National Institute of Informatics, Tokyo)
Philipp Wendler (LMU Munich)
Thomas Wies (New York University)
Enea Zaffanella (University of Parma)
Li Zhou (Max Planck Institute for Security and Privacy)