刷手机速览软件工程顶会新文-4篇FM 2026获奖论文

1. 异步团队自动机

Asynchronous Team Automata

• 作者: Davide Basile（[Formal Methods and Tools lab, CNR–ISTI, Italy]），Maurice H. ter Beek（[Formal Methods and Tools lab, CNR–ISTI, Italy]），José Proença（[CISTER & INESC TEC & University of Porto, Portugal]）
• 代码与数据集：A-Team GitHub；论文示例已集成于A-Team工具，无独立数据集。
• 关键词: 异步团队自动机（Asynchronous Team Automata）；多方通信（Multi-party Communication）；同步—异步交互（Synchronous–Asynchronous Interaction）；缓冲信道（Buffered Channels）；形式化验证（Formal Verification）
• 一句话速览: 提出异步团队自动机（ATeams），以位置化FIFO/多重集缓冲机制扩展传统Team Automata，在统一语义框架内同时刻画同步通信、异步通信以及多发送者—多接收者交互。
• 研究动机与技术挑战:
• 动机: 本文旨在解决现有Team Automata主要依赖同步通信、难以反映真实分布式网络中消息延迟、重排和异步传输行为的问题；这些行为可能直接影响死锁、因果一致性等性质。
• 挑战: 传统Team Automata难以描述异步消息传递，而CFSM及多数异步多方会话模型主要建立在点对点通信基础上，难以自然支持由同步类型约束的多发送者、多接收者通信；同时，不同缓冲位置和缓冲类型会显著改变系统可达行为与安全性质。
• 核心贡献与方法:
• 贡献: 本文提出Asynchronous Team Automata（ATeams）及其A-Team原型工具，并系统给出了语法、操作语义、良构性（well-formedness）与良行为性（well-behavedness）条件。
• 方法: 核心是在同步类型中显式引入同步/异步模式、缓冲类型及缓冲位置，支持sender、receiver、global和sender-receiver等不同缓冲作用域，并建立发送非阻塞、通信参与者约束和消息数量确定性等语义原则；进一步通过状态空间分析检测响应性、孤儿消息、无限缓冲及死锁等问题。
• 对标NSFC申请书:
• 科学目标: 面向异构同步—异步多方分布式系统中通信语义不统一与安全性质难以组合分析的问题，拟通过同步类型与位置化缓冲相结合的统一交互语义，揭示消息延迟、重排、缓冲策略与多方同步约束共同作用下的系统行为演化规律，发展可组合、可判定的多方通信验证理论体系，支撑复杂分布式协作系统的可信设计。
• 核心科学问题: 在参与者数量约束、缓冲位置/类型及消息重排共同变化的条件下，何种结构与语义条件能够保证多方异步系统的响应性、无孤儿消息和无死锁等关键性质，并在何种约束下能够恢复验证问题的可判定性？论文自身亦明确将异步死锁检测的可判定边界作为后续理论问题。

2. Pono 2.0：面向安全性与活性的通用SMT模型检验器

Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness

• 作者: Aron Ricardo Perez-Lopez（[Stanford University]），Po-Chun Chien（[Stanford University; LMU Munich]），et al.
• 代码与数据集：Pono GitHub；复现实验包（Zenodo）。
• 关键词: SMT模型检验（SMT-Based Model Checking）；安全性验证（Safety Verification）；活性验证（Liveness Verification）；Craig插值（Craig Interpolation）；反例引导抽象精化（CEGAR）
• 一句话速览: Pono 2.0构建了一个求解器无关、算法模块化的SMT模型检验平台，通过新增活性验证以及ISMC、DAR等插值式安全验证引擎，将多类安全/活性算法、抽象精化和不同SMT后端统一到同一验证基础设施中。
• 研究动机与技术挑战:
• 动机: 本文旨在提升理论丰富转移系统上模型检验的通用性、可扩展性和性能，特别是突破Pono 1.0主要针对安全属性的限制，使同一平台能够处理安全性与活性性质。
• 挑战: 不同系统可能涉及位向量、数组、整数和实数等不同背景理论，而BMC、插值、IC3/PDR及CEGAR等算法具有明显互补性；不同性质、理论和SMT求解器之间不存在单一稳定占优的验证配置。Pono 2.0因此同时扩展了VMT-LIB、活性性质、插值引擎、数组抽象和后端配置能力。
• 核心贡献与方法:
• 贡献: 本文发布Pono 2.0：增加Btor2活性验证、VMT-LIB前端、ISMC与DAR引擎，增强IMC、IC3SA和CEGAR，并将违例见证生成扩展至全部主要验证引擎。
• 方法: 在安全性方面，以Craig插值形成可达状态过近似：IMC采用反向插值和frontier-set简化，ISMC利用可复用的插值序列，DAR同时维护前向和后向可达近似；在活性方面，通过Liveness-to-Safety（L2S）*和k-liveness*将活性问题规约到既有安全验证基础设施。
• 对标NSFC申请书:
• 科学目标: 面向理论丰富、有限/无限状态转移系统的安全性与活性统一验证中算法适配性和求解性能高度不稳定的问题，拟通过“性质规约—状态抽象—双向可达近似—SMT求解”协同机制，揭示不同背景理论、系统结构与验证算法之间的适配和收敛规律，发展自适应、可扩展的统一模型检验方法体系，支撑复杂软硬件系统的高可信验证。
• 核心科学问题: 在状态空间结构、背景理论和待验证性质不断变化的条件下，如何刻画插值、IC3/PDR、CEGAR及不同SMT求解器之间的互补机制，并据此获得具有稳定收敛性和可预测性能的验证策略？

3. 面向门连接交互模型组合的特化反统一方法

Specializing Anti-unification for Interaction Models Composition via Gate Connections

• 作者: Joel Nguetoum（[Université Paris-Saclay, CEA List; CentraleSupélec, MICS]），Boutheina Bannour（[Université Paris-Saclay, CEA List]），et al.
• 代码与数据集：FM 2026实验Artifact（Zenodo）。
• 关键词: 交互模型组合（Interaction Model Composition）；反统一（Anti-unification）；特殊常量保持（Special-Constant Preservation）；等式理论（Equational Theories）；门连接（Gate Connections）
• 一句话速览: 提出特殊常量保持反统一（sc-preserving anti-unification），将跨局部交互视图的通信连接编码为不可被泛化掉的“gate”常量，从而在结合律、交换律和单位元等代数等价关系下重构语义一致的全局交互模型。
• 研究动机与技术挑战:
• 动机: 本文旨在解决分布式系统的多个局部交互模型如何自动组合为结构一致、通信连接正确且保留局部行为的全局交互模型这一问题。
• 挑战: 标准反统一会将局部项中的结构差异抽象为变量，可能同时把必须保留的跨视图通信连接泛化掉；另一方面，seq、alt、par等交互算子具有结合、交换、单位元等代数性质，使“结构相同”不能仅依赖纯语法匹配。
• 核心贡献与方法:
• 贡献: 本文建立了特殊常量保持反统一理论，给出最小一般泛化的存在/唯一性条件以及终止性、可靠性（soundness）和完备性证明，并扩展到模等式理论的情形。
• 方法: 首先将匹配的发送—接收动作替换为共享gate特殊常量，再执行受约束的Decompose、Solve和Recover规则；其中Solve禁止通过变量替换引入特殊常量，并利用failure conflict positions提前识别无解情形。完成反统一后，通过替换与value-passing重新实例化gate得到全局模型；投影定理证明组合模型分别投影至两个局部lifeline集合后，与原局部模型在等式理论下保持等价。
• 对标NSFC申请书:
• 科学目标: 面向分布式系统多源局部交互模型在代数等价与接口约束下难以一致组合的问题，拟通过“受约束结构泛化—接口常量保持—语义投影等价”的理论视角，揭示局部结构差异、跨组件连接约束与全局行为重构之间的内在关系，建立具有存在性、完备性和行为保持保证的交互模型组合理论，支撑开放分布式系统的自动化建模与演化。
• 核心科学问题: 在结合性、交换性、单位元等代数等价以及跨视图gate必须保持的双重约束下，何种结构冲突决定最具体全局泛化模型的存在性与可计算性，如何保证组合后的全局模型投影后与各局部模型保持行为语义一致？

4. 基于分布不变式的采样算法验证

Verifying Sampling Algorithms via Distributional Invariants

• 作者: Daniel Zilken（[RWTH Aachen University]），Kevin Batz（[University College London]），et al.
• 代码与数据集： 代码/数据集未公开；论文主要贡献为形式化理论、证明及FDR/FLDR验证案例，正文与附录未提供专用代码仓库或实验数据集链接。
• 关键词: 采样算法验证（Sampler Verification）；概率程序（Probabilistic Programs）；分布不变式（Distributional Invariants）；Hoare逻辑（Hoare Logic）；参数化采样（Parameterized Sampling）
• 一句话速览: 提出面向概率程序的类Hoare分布不变式验证框架，把程序状态上的概率分布视为一等语义对象，从而首次系统地对参数化Fast Dice Roller和Fast Loaded Dice Roller给出部分正确性与完全正确性的形式化证明。
• 研究动机与技术挑战:
• 动机: 本文旨在解决随机采样算法能否精确产生指定目标分布的功能正确性验证问题，这类算法直接服务于随机算法、仿真以及机器学习。
• 挑战: 采样程序存在三重困难：目标概率必须被精确证明而非近似；循环中的目标分布可能只有在无限迭代极限才形成；输入参数又会诱导无限族概率模型。传统基于状态的概率验证难以直接表达这类分布级性质。
• 核心贡献与方法:
• 贡献: 本文将Markov链上的分布不变式严格提升到概率程序层面，建立程序分布不变式与其操作Markov链分布不变式之间的等价关系，并补充分布式Hoare循环规则和可逆/单射赋值推理技术；最终完成FDR与FLDR两个非平凡参数化采样器的形式化验证。
• 方法: 将概率程序解释为分布变换器，以分布集合描述strongest postcondition和有限步可达分布，再利用归纳分布不变式约束整个概率演化过程；通过ω-闭包把有限步可达分布连接到循环的极限输出分布，并结合几乎必然终止（AST）由部分正确性提升为完全正确性。FDR的不变式刻画输出索引的均匀概率结构，FLDR进一步约束二叉采样树中“当前及未来”输出概率质量。
• 对标NSFC申请书:
• 科学目标: 面向含无界概率循环和参数化输入的随机采样程序难以精确验证目标分布的问题，拟通过将状态分布提升为程序的一阶语义对象并构造可归纳分布不变式，揭示有限步可达分布、极限输出分布与几乎必然终止之间的内在联系，发展可自动化的概率程序定量正确性验证理论与不变式推理体系，支撑机器学习和随机算法中基础采样组件的可信性。
• 核心科学问题: 在目标分布只有经无限概率迭代才能形成、且输入参数诱导无限模型族的条件下，如何构造有限可表示且可归纳验证的分布不变式，使有限步局部推理能够严格蕴含极限输出分布的全局精确性？论文进一步指出，面向分布的断言语言与不变式自动化是这一方向的重要后续问题。