VMCAI 为验证、模型检查和抽象解释领域的研究人员提供了一个论坛，促进了这些领域及相关领域的互动、交叉融合和混合方法的进步。VMCAI 2025 将是该系列的第 25 届。VMCAI 将于 2025 年 1 月 20 日至 21 日以线下活动形式举行。每篇被录用的论文需至少一名作者注册参会并现场发表论文。

1、组委会

联合主席：
Shankaranarayanan Krishna 印度孟买理工学院
Sriram Sankaranarayanan 科罗拉多大学博尔德分校 美国
Ashutosh Trivedi 科罗拉多大学博尔德分校 美国
文物评估联合主席：
Ernst Moritz Hahn 特温特大学 荷兰
Andrea Turrini 中国科学院软件研究所 中国

程序委员会主席：
Sriram Sankaranarayanan（University of Colorado, Boulder, USA）
Krishna Shankaranarayanan（IIT Bombay, India）
Ashutosh Trivedi（University of Colorado Boulder, USA）

2、出版信息

工件评估委员会仅将提交的工件用于工件评估。评估期间或评估结束后，委员会不得公开该工件或其任何部分。工件及其所有相关数据将在评估过程结束时删除。我们鼓励工件作者将其工件永久公开，并通过 DOI 在其论文中引用它们。所有存在 DOI 且工件评估委员会已知的工件，均会被授予可用性徽章。

• 程序验证
• 模型检查
• 抽象解释
• 抽象域
• 程序综合
• 静态分析
• 类型系统
• 演绎法
• 程序逻辑
• 一阶理论
• 决策程序
• 插值
• 霍恩条款求解
• 项目认证
• 分离逻辑
• 概率规划与分析
• 错误诊断
• 检测错误和安全漏洞
• 程序转换
• 混合和信息物理系统
• 并发和分布式系统
• 数值特性分析
• 智能合约分析
• 神经网络分析
• 关于上述所有主题的案例研究

1、征文

VMCAI 2025 是第 26 届验证、模型检查和抽象解释国际会议。会议将于 2025 年 1 月 20 日至 21 日举行。VMCAI 为验证、模型检查和抽象解释领域的研究人员提供了一个论坛，促进这些领域及相关领域的互动、交叉融合和混合方法的进步。

2、重要日期

• 2024 年 10 月 1 日AOE：论文提交截止日期（延长）。
• 2024 年 11 月 11 日：通知
• 2024 年 11 月 22 日：发布照相排版版本

3、提交

投稿须遵循 Springer 的 LNCS 格式。页数限制取决于论文类别（见下文）。每个类别中，超出页数限制的额外内容可能会被放置在清晰标记的附录中，由审稿人酌情阅读，并在最终版本中省略。格式样式文件及其他格式指南可在Springer 网站找到。投稿可通过EasyChair进行。注意：投稿将于 8 月 26 日开放。

所有被录用的论文将发表于 Springer 的《计算机科学讲义》系列丛书。每篇论文的通讯作者需填写并签署一份出版许可表格，并与照相排版版本一并提交。

投稿将进行单盲评审。投稿内容不得匿名，以备审核。论文将分为三类：常规论文、工具论文和案例研究。每类论文的页数限制不同，评审方式也有所不同。

常规论文清晰地阐述并论证验证、摘要解释或模型检验领域的进展。如适用，需提供实验验证。常规论文篇幅限制为 20 页，采用 LNCS 格式，不计参考文献。

工具类论文应介绍一种新工具、新的工具组件或现有工具的新颖扩展。论文应简要描述其理论基础并附上相关引文，并强调设计和实现方面的问题，包括软件架构和核心数据结构。一篇常规的工具类论文应清晰地阐述工具的功能，结合工具可处理的问题类型和规模讨论其实际能力，描述实际案例研究的经验，并在适用的情况下提供严格的实验评估。介绍现有工具扩展的论文应明确侧重于工具相对于先前发布版本的改进或扩展，最好能提供资源和功能增强方面的数据佐证。强烈建议作者公开其工具并提交成果。工具类论文限12页，采用LNCS格式，不计参考文献。

4、投稿内容

您的工件档案文件必须包含以下内容：

主要工件，即复制论文结果所需的数据、软件、库、脚本等。
我们建议您为用户提供易于使用的脚本来重现和分析结果，即使用预期配置运行工具的脚本和将其结果可视化为表格/图表的脚本。
审核将采用单盲方式。请确保您不会（意外地）获知审核者的身份（例如，通过分析、日志记录）。
来自您的实验的日志。
通过日志和适当的分析脚本，我们可以轻松匹配论文中报告的结果。
一个LICENSE文件。您的许可证需要允许工件评估主席下载并分发该工件给工件评估委员会成员，并且必须允许工件评估委员会成员评估该工件，例如，为了工件评估的目的使用、执行和修改该工件。
向用户介绍工件README.pdf并指导用户复制结果的文档。理想情况下，它应该包含以下部分：
一份入门指南，详细说明如何设置工件并准备复制论文结果。如果您不仅在主要评审阶段，还在测试阶段为评审员提供支持，我们将不胜感激。为此，提供安装和初步测试（即，以可能出现技术难题的方式）的说明，以及此类初步测试的预期结果（以了解测试是否成功）将非常有帮助。
复制论文结果的 分步说明。
请记录论文中哪些主张或结果可以通过该成果复制，以及如何复制（例如，必须进行哪些实验）。同时，请解释哪些主张和结果无法复制，以及原因。
详细描述如何复制论文结果，尤其要描述复制结果所需的步骤。为了简化评审流程，我们建议提供评估脚本（如适用）。
准确说明您用于测试工件的资源需求（RAM、核心数、CPU 频率等）。
提供运行实验所需时间的粗略估计。
对于需要大量资源（硬件或时间）的任务，我们建议提供在合理适度的资源和时间限制下复制部分结果的可能性，例如，在配备 8 GB RAM 的个人计算机上，在 8 小时内完成。在这种情况下，请同时提供一个仅复制部分结果的脚本。