计算机辅助设计的形式方法(FMCAD2025)

   VSTTE会议系列的目标是通过理论发展、工具演进和实验验证的互动，推动软件验证科学与技术的进步。由Tony Hoare和Jayadev Misra领导的验证软件倡议（VSI）是一个雄心勃勃的研究项目，旨在将大规模验证软件变为实际可行。国际验证软件会议：理论、工具与实验（VSTTE）是推动该倡议的主要论坛。VSTTE汇聚了软件验证领域各领域的专家，促进国际合作，共同应对关键研究挑战。理论工作包括规范与验证的语义基础与逻辑，以及验证算法和方法论。这些工具涵盖了规范和注释语言、程序分析器、模型检查器、交互式验证器和证明检查器、自动定理证明器和SAT/SMT求解器，以及集成的验证环境。实验工作通过承担涵盖硬件、操作系统、编译器、计算机安全、并行计算和网络物理系统的重要规范/验证工作，推动理论与工具的研究议程.

组委会：

项目主席

• 布鲁诺·杜特雷，AWS，美国
• 贝蒂娜·柯尼霍弗，奥地利格拉茨工业大学

学生论坛主席

• 坦娅·辛德勒，瑞士巴塞尔大学
• 李·A·巴内特，AWS，美国

出版主席

• 乔治·魏森巴赫，奥地利维也纳工业大学

宣传主席

• 马丁·塔普勒，奥地利维也纳理工大学

网络主席

• 斯特凡·普兰格，奥地利格拉茨工科大学
• 托马斯·哈德，奥地利维也纳工业大学

关注的主题包括（但不限于）：

• 模型检查、定理证明、等价检查、抽象与约简、合成方法、位和字层的决策过程、概率方法、演绎方法与决策过程的组合。
• 计算机系统描述的综合与编译、建模、规范和实现语言、语言及其子集的形式语义、基于模型的设计、设计推导与转换、构造纠正方法。
• 将形式和半形式方法应用于硬件和软件的功能性和非功能性规格与验证，包括时序和功耗建模、计算系统各层次抽象验证、嵌入式系统、网络物理系统、汽车系统及其他安全关键系统的系统级设计与验证、硬件-软件协同设计与验证，以及事务级验证。
• 在工业规模设计中应用正式和半形式方法的经验;代表形式验证赋能、新功能或形式方法自动化的实质性改进的工具。
• 将正式方法应用于验证网络、分布式系统、智能合约、区块链和物联网设备的安全性、连接性和安全性属性。
• 对数据驱动的人工智能系统进行正式验证，涵盖安全性、对对抗输入的鲁棒性、可靠性、公平性以及合规性。
• 人工智能在增强形式方法技术上的应用，包括不变推断和规范推断、基于学习的验证与综合启发式方法，以及数据驱动的验证工作流程。