图灵奖得主Joseph Sifakis：将模型检测从学术应用至产业界的功臣 | CCF-GAIR 2018

软件工程专业的同学想必都很熟悉下面这起惨剧：1996 年 6 月 4 日，由欧洲 12 国联合研制的阿丽亚娜 (Ariane) 5 型运载火箭，在首次发射后因为一行代码的溢出错误导致火箭升空约 37 秒时爆炸，造价几亿欧元的火箭就这样悲剧收场。

如此重大的发射任务事前势必经过了周密的检查，但为什么还是没能避免惨剧的发生？举个例子大家就懂了，这就好比箭已离弦，导弹飞机离地升空，根本不可能在空中进行重启操作。再加上如火箭、飞机这样的军工，航天领域应用的软件代码越来越复杂，一旦发生代码溢出和死循环，后果也将越发不可承受。同样的悲剧也绝非孤例，微软的 Windows Azure 因受到一个闰日缺陷而宕机长达 30 多小时；亚马逊平台故障导致 0.07% 的用户数据最终无法复原。

在这样的背景下，学术界和工业界开始要求在常规测试之外采用更加严格