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

VMCAI 2025 will take place during January 20-21, 2025 as a physical (in-person) event. For each accepted paper at least one author is required to register for the conference and present the paper in person.

Submission Guidelines

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 is via EasyChair. Note: submissions will open on August 26th.

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

Call for Artifacts

VMCAI 2025 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. 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.

Artifact evaluation is single blind, artifacts should not be anonymous.

More information on artifact submissions can be found at https://conf.researchr.org/home/VMCAI-2025. 

List of Topics

The program 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.

Committees

Program Committee

• Abdulla, Parosh Aziz - Uppsala University, Sweden  
• Anastasiadi, Elli - Uppsala University, Sweden  
• Barbosa, Haniel - Universidade Federal de Minas Gerais, Brazil  
• Bouajjani, Ahmed - IRIF, Université Paris Diderot, France  
• Chakraborty, Soham - TU Delft, Netherlands  
• Chen, Xin - University of New Mexico, USA, United States  
• Cousot, Patrick  D'Antoni,
• Loris - UCSD, United States  
• D'Silva, Deepak - IISc Bangalore, India  
• D'Silva, Vijay - Google Inc.  
• Deshmukh, Jyotirmoy - University of Southern California  
• Giacobazzi, Roberto - University of Arizona, United States  
• Goharshady, Amir Kafshdar - Hong Kong University of Science and Technology, Hong Kong  
• Golia, Priyanka - Indian Institute of Technology, Kanpur, India and National University of Singapore, Singapore  
• Goubault, Eric - Ecole Polytechnique  
• Guha, Shibashis - Tata Institute of Fundamental Research, India  
• Gupta, Ashutosh - Indian Institute of Technology Bombay, India  
• Ivancic, Franjo - Google, United States  
• Jakobs, Marie-Christine - LMU Munich, Germany  
• Jha, Sumit - Florida International University, USA, United States  
• Kafshdar Goharshady, Amir - Hong Kong University of Science and Technology, Hong Kong  
• Kosaian, Katherine - Carnegie Mellon University  
• Kretinsky, Jan - Masaryk University, Czech Republic  
• Kunčak, Viktor - EPFL, Switzerland  
• Mallik, Kaushik - IST Austria, Austria  
• Mangal, Ravi - Colorado State University, United States  
• Mercer, Eric - Brigham Young University, United States  
• Meyer, Roland - TU Braunschweig, Germany  
• Miné, Antoine - Sorbonne Université, France  
• Mover, Sergio - École Polytechnique, France  
• Muroya, Koko - RIMS, Kyoto University, Japan  
• Oliveira Da Costa, Ana - IST Austria, Austria  
• Pavlogiannis, Andreas - Aarhus University, Denmark  
• Podelski, Andreas - University of Freiburg, Germany  
• Prabhu, Vinayak - Colorado State University, United States  
• Rival, Xavier - Inria; ENS; CNRS; PSL University, France  
• Rümmer, Philipp - University of Regensburg and Uppsala University  
• Sankaranarayanan, Sriram - University of Colorado, Boulder, United States  
• Schewe, Sven - University of Liverpool  
• Shankaranarayanan Krishna - Indian Institute of Technology Bombay, India  
• Sharma, Subodh - IIT Delhi, India  
• Somenzi, Fabio - University of Colorado Boulder, USA  
• Sridhar, Meera - University of North Carolina Charlotte, USA  
• Srivathsan, B - Chennai Mathematical Institute, India  
• Thakur, Aditya V. - University of California at Davis, United States  
• Tizpaz-Niari, Saeid - University of Texas at El Paso, United States  
• Trivedi, Ashutosh - University of Colorado Boulder, United States  
• Wang, Chao - University of Southern California, United States  
• Wojciechowski, Piotr - West Virginia University, USA, United States  
• Wojtczak, Dominik  Žikelić, Đorđe - Singapore Management University, Singapore  
• Zhang, Zhen - Utah State University, United States  

Organizing committee

• Sankaranarayanan, Sriram  (University of Colorado, Boulder, United States) PC Co-Chair
• Shankaranarayanan Krishna (Indian Institute of Technology Bombay, India) PC Co-Chair
• Trivedi, Ashutosh  (University of Colorado Boulder, United States) PC Co-Chair
• Hahn, Ernst Moritz (University of Twente, NL) AEC Co-Chair
• Turrini, Andrea (State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences) AEC Co-Chair

Publication

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.

Venue

VMCAI 2025 will be held in Denver, Colorado, United States. The conference is co-located with POPL 2025. 

Contact

All questions about submissions should be emailed to the PC co-chairs Sriram Sankaranarayanan, Krishna Shankaranarayanan, and Ashutosh Trivedi.