- C 分析器：C 程序的静态程序分析工具
基于抽象解释技术的 C 程序静态分析工具，支持多种抽象域，能够对声明、赋值、二进制操作、条件语句、循环等 C 语言构造进行分析，但不支持数组、结构体、联合体、指针或函数调用。
- 面向自动化系统安全评估的形式化故障注入
通过将形式化方法和故障注入相融合，增强自主系统的可靠性，并通过这种更加紧密的联系，为安全可靠的自动化系统的开发铺平道路。
- 第五届自主系统形式化方法国际研讨会论文集
这篇研究论文总结了第五届自主系统形式方法国际研讨会的会议情况和论文接收结果，展示了该会议作为自主系统的形式建模和验证研究领域的知名出版场所的发展趋势。
- 自主系统的形式方法
给出关于应用形式方法于自治系统领域的当前最新研究状态的概述，包括系统的合成、不确定性的概念、采用形式方法的学习系统的行为界限、系统的监测以及形式方法在强化学习、不确定性、隐私、可解释性、规制和认证方面的未来发展方向。
- 运行时监测基于深度学习的感知
深度神经网络在复杂感知系统方面起着重要作用，但为了确保其功能不足不会造成危害，除了静态验证和测试方法外，还需要运行时验证技术来检测关键事件、诊断问题并强制执行要求。本教程介绍了文献中提出的技术方法，包括机器学习界经典方法和形式方法界的一些技 - 正式 - DAgger 用于 MCTS：使用形式方法的数据聚合实现更低延迟的蒙特卡洛树搜索
我们研究如何高效地结合形式方法、蒙特卡洛树搜索 (Monte Carlo Tree Search，MCTS) 和深度学习，以在大型马尔可夫决策过程 (Markov Decision processes，MDPs) 中生成高质量的滞后视野策略 - MM可扩展概率路径
本文提出了一种使用决策图与概率值增强的线性编码路线预测方法，将预测速度提升一倍，并且在真实路网中的性能显著优于现有技术。
- 由时序逻辑信号规范引导的多智能体强化学习
本论文提出了一种新的基于 STL 模板的多智能体强化学习算法以指导奖励设计，实验证明相比没有 STL 指导的情况下，算法能够显著提高多智能体系统的性能和安全性。
- STL: 对系统验证而言意外棘手的逻辑
人类实验发现形式化方法的规范并不是本质上能够被人类理解的，而且验收正确性受到多种因素的影响，提出了在规范展示和验收培训中应当考虑人体工程学改进的建议。
- 使用形式化方法证明 XAI 神话 -- 初步结果
这篇研究论文探讨了可解释人工智能的重要性以及存在的困境和误解，通过形式化方法来反驳这些误解并提出实际有效的替代方法。
- 第三届神经网络验证大赛（VNN-COMP 2022）：概述与结果
这篇文章总结了第三届国际神经网络验证竞赛（VNN-COMP 2022），它是第 5 届面向机器学习自主系统的形式方法研讨会（FoMLAS）的一部分，旨在促进当前最先进的神经网络验证工具的公平客观比较，鼓励工具接口的标准化，并聚集神经网络验证 - 从智能代理到值得信赖的以人为中心的多智能体系统
南安普顿大学的代理、交互与复杂性研究小组在多智能体系统 (MAS) 领域有着悠久的研究历史，已经在 MAS 学习、协调智能体系统的博弈论技术、表示和推理的形式方法等方面做出了实质性的科学贡献。该文重点介绍了该小组取得的关键成果，并详细阐述了 - 第四届自主系统形式化方法国际研讨会（FMAS）和第四届自动化可验证软件系统开发国际研讨会（ASYDE）论文集
本文介绍了 2022 年第四届自主系统形式化方法国际研讨会（FMAS 2022）和第四届自动化和可验证软件系统开发国际研讨会（ASYDE 2022）的联合论文集。该研讨会目的在于汇聚使用形式化方法解决自主系统所带来独特挑战的研究者，探讨在形 - 协变 - 逆变细化模态 $μ$- 演算
本文介绍了一种新的模态 mu - 演算系统 CCRML^μ，该系统由模态 Mu - 演算系统 K^μ 添加 CC-refinement 量词而得到。CCRML^μ 可用于规范化一些关于反应和生成动作的系统性质的问题，是一种描述系统性质的规范 - 在纯过去时线性时态逻辑中规划具有时间延伸目标：多项式约减为标准规划
研究纯过去时线性时态逻辑（PPLTL）中表达的时间上延长的目标，这对于表达目标特别有趣，因为它允许表达形式方法文献中的复杂任务，同时在确定性和非确定性领域的规划的最坏情况的计算复杂性仍然与经典可达性目标相同。本文提出了一种将 PPLTL 目 - 具算术的数据感知动态系统的线性时间验证
本文研究了数据感知动态系统的模型和验证，并将其扩展为线性算术。我们提出了 “有限总结” 的新语义属性，展示了有限总结对于 DDS 的线性时间、有限跟踪性质的证明是可判定的，并且展现了有限总结在形式方法和数据库理论中的具体应用。此外，我们展示 - 自主驾驶汽车的正式场景测试：从仿真到现实世界
本文提出了一种基于形式化方法的智能汽车自动场景测试的新方法，结合仿真和实际测试，并通过实验验证形式化仿真可以有效识别可在跑道上运行的测试用例，仿真和真实世界之间的差距可以得到系统评估和弥合。
- 基于物理的攻击在网络物理系统中的形式化方法（扩展版）
运用形式化方法对 Cyber-Physical Systems 中受物理攻击的传感器和执行器进行完整性和拒绝服务攻击的形式化处理，提出了威胁模型，度量攻击成功率，使用 Uppaal SMC 作为静态安全性分析工具进行实例分析。
- 实现可验证的人工智能
本文从形式方法的角度考虑了 “可验证的人工智能” 这一目标。描述了实现可验证人工智能所面临的五个挑战及相应的五个解决原则。
- MM加速科学：计算研究议程
大数据和算法处理促进科学进步，但需要研究算法处理和认知工具的发展，以及如何在科学领域中进行有效的数据分析和模拟，以推进科学发现的速度和准确性。