11月24日，新葡萄荣幸邀请到浙江大学计算机科学与技术学院赵永望教授，为我们带来了一场题为“安全攸关软件形式化验证工具探索”的学术讲座活动。讲座由新葡萄院长丁佐华教授主持，新葡萄部分师生代表参与。
安全攸关软件是一类其错误/故障可能导致系统失效，进而引发严重生命和财产损失的软件。形式化验证已经成为工业界确保安全攸关软件正确性和安全性的主要手段之一。赵永望教授针对当前业界形式化验证工具存在技术门槛高、易用性低、适用面有限等问题，介绍了一系列由他团队自研的形式化验证工具，包括定理证明云平台、源码自动化验证工具、符合CC标准的形式化框架等。他详细阐述了这些工具的实际应用及存在的不足，并深入讨论了形式化验证工具研发的一些观点。
讲座结束后，赵永望教授与新葡萄师生展开了互动交流。新葡萄师生对安全攸关软件形式化验证的研究内容以及未来发展方向有了更深入的理解。这次学术交流为新葡萄师生提供了宝贵的学术启示，促使他们对形式化验证领域的研究产生更浓厚的兴趣。
