12月9日上午，数据工程与知识工程教育部重点实验室举办第3期德科前沿技术讲座。本期讲座的主题为“基于路径空间遍历的有界验证途径及其应用”，由南京大学软件学院卜磊教授主讲，由数据工程与知识工程教育部重点实验室范举教授主持。

讲座伊始，范举教授对报告人和参与师生表示欢迎，并详细介绍了讲座报告人的研究领域及成果。

卜磊教授首先阐述了基于路径遍历的有界验证方法的研究背景。在现代软件系统日益复杂的背景下，尤其是涉及安全敏感领域（如高铁、飞机、医疗手术等）的系统，保障软件的可信性与安全性变得愈加重要。系统故障可能导致灾难性后果，因此形式化验证成为确保系统安全性的重要手段。形式化验证旨在通过数学模型与代码验证系统的正确性，防止致命错误的发生。然而，形式化验证面临的挑战之一是可达性检验，尤其是在全局验证与有界验证之间的复杂性问题上。尽管有界验证通过限制验证的状态空间深度有效地减小了问题规模，但高复杂度和低效率等问题依然限制了其在工业界的实际应用。

接下来，卜磊教授详细介绍了基于路径遍历的有界验证方法。为了解决有界验证中的复杂性问题，其团队提出了一种全新的路径遍历验证方法。该方法通过单路径状态空间编码和路径验证，成功地将系统的复杂性分解。团队首先采用路径空间约减和复杂约束求解技术优化验证过程，有效解决了路径求解中的效率瓶颈。此外，针对混成系统的有界验证，团队还提出了新的技术手段，如不可解子约束集定位技术，大大提升了验证效率和准确性。实验结果表明，这一方法在国际软件验证竞赛（SV-COMP）中表现突出，在Java赛道中获得第一。

在研究应用方面，卜磊教授将基于路径的有界验证方法应用于复杂系统的运行时监控。在列车控制系统（CPS）的场景中，传统的离线验证方法往往难以应对系统状态随实时参数变化的情况。为此，其团队构建了一个运行时参数计算模型，能够实时处理并验证系统的状态行为。通过结合路径遍历技术，该方法不仅能保证系统的安全性，还大幅提高了验证效率，在较短的时间内完成复杂系统的验证。该技术已经扩展应用于机械臂轨迹验证、自动驾驶和轨道交通等领域，展现出广泛的应用前景。卜磊教授还计划推广该技术在不同领域应用，包括机械臂轨迹验证与控制、自动驾驶等。

最后，卜磊教授对基于路径遍历的有界验证方法进行了总结和展望。该研究突破了有界验证中的复杂性控制难题，提出了新的验证工具BACH与验证方法，并在多个实际应用场景中取得了显著成果。该方法不仅为复杂软件系统的有界验证提供了有效的解决方案，也推动了形式化验证技术在工业界的应用。未来，团队将继续优化现有技术，进一步提高验证效率与精度，并探索其在更多领域的扩展应用。

讲座后，老师和同学们就讲座内容，与卜磊教授展开了热烈讨论和交流。本期德科前沿技术讲座圆满结束。