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

VMCAI 2027 will take place on January 11–12, 2027 as a physical (in-person) event in Mexico City, Mexico, co-located with POPL 2027. For each accepted paper, at least one author is required to register for the conference and present the paper in person.

List of Topics

The program will consist of refereed research papers as well as invited talks. Research contributions may report new results, 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 must follow the Springer LNCS format. Please refer to Springer’s author instructions and templates.

Submission is via EasyChair: https://easychair.org/conferences/?conf=vmcai2027

All accepted papers will be published in Springer’s Lecture Notes in Computer Science (LNCS) series. The corresponding author of each accepted paper must complete and sign a License-to-Publish form when submitting the camera-ready version.

Paper Categories

*Page limits exclude references.

Regular Papers

Regular papers should clearly identify and justify an advance in the field of verification, abstract interpretation, or model checking. Where applicable, they should be supported by experimental validation.

Regular papers should contain original research and sufficient detail to assess the merits and relevance of the contribution. They will be evaluated on the basis of a combination of correctness, technical depth, significance, novelty, clarity, and elegance.

Tool Papers

Tool papers should 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 design and implementation concerns, including software architecture and core data structures.

A tool paper should give a clear account of the tool’s functionality, discuss its 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 presenting extensions to existing tools should clearly focus on the improvements or extensions with respect to previously published versions, 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.

Case Studies

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 lessons learned from this technology transfer experience. Shorter case study papers are also welcome.

Review Process

Regular paper submissions will undergo a double-blind review process.

Authors submitting regular papers should ensure that their manuscripts are properly anonymized.

Artifacts

VMCAI 2027 offers authors the option to submit an artifact alongside their paper. Artifacts include any additional material that substantiates the claims made in the paper and, ideally, enables the reported results to be fully reproducible.

Artifact evaluation is conducted alongside the paper review, and its outcome may influence the final acceptance decision.

Authors of tool papers are strongly encouraged to make their tools publicly available and submit an artifact.

Additional Information

• References do not count toward the page limit.
• Authors may include a clearly marked appendix after the references. Appendices are not subject to the page limit, but reviewers are not required to read them.
• Simultaneous submissions to other conferences with proceedings, or submissions of material that has already been published elsewhere, are not permitted.