圖靈獎得主Joseph Sifakis：將模型檢測從學術應用至產業界的功臣 | CCF-GAIR 2018

軟件工程專業的同學想必都很熟悉下面這起慘劇：1996 年 6 月 4 日，由歐洲 12 國聯合研製的阿麗亞娜 (Ariane) 5 型運載火箭，在首次發射後因爲一行代碼的溢出錯誤導致火箭升空約 37 秒時爆炸，造價幾億歐元的火箭就這樣悲劇收場。 如此重大的發射任務事前勢必經過了周密的檢查，但爲什麼還是沒能避免慘劇的發生？舉個例子大家就懂了，這就好比箭已離弦，導彈飛機離地升空，根本不可能在空中進行重

>>阅读原文<<