4月19日，應基礎軟件國家工程研究中心實驗室邀請，2007年ACM圖靈獎獲得者Edmund M.Clarke教授到軟件所進行訪問，并作題為Turing's Computable Real Numbers and Why They Are Still Important Today的學術講座，講座由楊秋松副研究員主持。來自中科院、北京大學、北京信息科技大學等院校的40余名老師和學生聆聽了報告。

Clarke教授報告了其研究組在混成系統驗證方面的最新工作。安全關鍵領域的許多應用系統（比如汽車自動機駕駛、民航飛機碰撞檢測、高速列車控制以及生物醫學系統等），其本質上是混成系統，即包含了離散狀態變量和根據時間按特定動力學規律變化的連續變量。混成系統的驗證具有很高的復雜度，特別是當描述動力學規律的微分方程為非線性函數（比如指數、三角函數）時，該問題是不可判定的。針對該問題， Clarke教授研究組提出了基于符號化和數字計算的近似判定算法：對于非線性實數理論下的一階邏輯公式，若非線性函數是Turing Type 2 可計算的，則可以給出近似delta判定結論，且該delta一般非常小，從而保證該結論一般情況下都成立。

Clarke教授生動報告激起了與會人員的濃厚興趣，大家對混成系統驗證和近似SMT判定過程十分關注。報告結束后，與會人員踴躍提問，Clarke教授就相關問題也一一給予回答。

Clarke現任美國卡內基梅隆大學計算機科學系教授、ACM和IEEE會士。他在軟硬件驗證、自動定理證明、形式方法等方面享有崇高的國際聲譽，是模型檢驗方法的開創者之一，2007年獲ACM圖靈獎。

Edmund M.Clarke教授作報告

講座現場