形式化方法賦能計算機其他領(lǐng)域|CCF數(shù)圖焦點第39期
編者寄語
形式化方法是具有嚴(yán)格數(shù)學(xué)基礎(chǔ)的保障計算機軟硬件正確性與安全性的方法,在近20年取得了長足進步,已經(jīng)在國內(nèi)外頭部公司(比如微軟、亞馬遜、華為等)取得了成功應(yīng)用。
形式化方法經(jīng)過幾十年已經(jīng)發(fā)展出了多種技術(shù),包括約束求解、模型檢測、定理證明、抽象解釋等。形式化方法的應(yīng)用領(lǐng)域也不斷擴展,包括芯片設(shè)計驗證、操作系統(tǒng)驗證、編譯器驗證、網(wǎng)絡(luò)驗證、區(qū)塊鏈智能合約驗證、數(shù)據(jù)庫查詢等價性驗證、智能系統(tǒng)驗證等。而且近年來,形式化方法作為人工智能符號學(xué)派的代表,如何和以深度學(xué)習(xí)為代表的人工智能統(tǒng)計學(xué)派進行交叉融合,已經(jīng)成為研究熱點和難點。
本次專題聚焦形式化方法賦能計算機其他領(lǐng)域,將CCF數(shù)字圖書館相關(guān)報告視頻和期刊文章資源以及其他平臺與選題相關(guān)的資源進行聚合,方便會員集中觀看學(xué)習(xí),也為讀者探索形式化方法與計算機其他領(lǐng)域的交叉融合拋磚引玉。
目錄
本期主編:吳志林 CCF形式化方法專委秘書長 中國科學(xué)院軟件研究所研究員
往期回顧