VMCAI 2026 : Verification, Model Checking and Abstract Interpretation
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 will be via EasyChair. Submissions will undergo a single-blind review process. 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. 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. Case study papers are restricted to 20 pages in LNCS format, not counting references. (Shorter case study papers are also welcome.)
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.
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 will be via EasyChair. Submissions will undergo a single-blind review process. 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. 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. Case study papers are restricted to 20 pages in LNCS format, not counting references. (Shorter case study papers are also welcome.)
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.