铸就理论基石验证系统逻辑——记上海交通大学电子信息与电气工程学院特别副研究员符鸿飞

摘要

"实践是检验真理的唯一标准",很多软件、系统在开发时都会进行模拟验证,以确保顺利运行。然而近些年来,模拟验证的短板逐渐凸显--伴随着计算机的飞速发展,越来越多超大规模设计出现,对于这些设计来说,仿真挑战过于耗费时间,从理论上进行测试反而更为合适。这种测试被称为"形式化验证",是一种穷尽式数学技术,其原理是利用数学和逻辑的方法来证明计算机系统的正确性。