本期新增術語新詞：可滿足性模理論(Satisfiability modulo theories)。
開篇導語：
本期新增術語新詞：可滿足性模理論(Satisfiability modulo theories)。可滿足性模理論指函數和關系符号在背景理論中進行解釋的謂詞邏輯公式的可滿足性判定問題。
可滿足性模理論(Satisfiability modulo theories)
作者：吳志林、馬菲菲、蔡少偉（中國科學院軟體研究所）
InfoBox：
中文名：可滿足性模理論
外文名：Satisfiability modulo theories
簡寫：SMT
學科：計算機軟體與理論
基本簡介：
可滿足性模理論的基本思想是針對多種資料類型和相應的謂詞邏輯理論，提出一個一般的架構，使得可以求解特定背景理論下的謂詞邏輯公式的可滿足性判定問題，進一步，可以求解涵蓋多種理論的混合邏輯公式的可滿足性判定問題。可滿足性模理論與互動式定理證明相比，能夠處理的邏輯公式要少一些，一般考慮無量詞或者量詞嵌套較少的謂詞邏輯公式，但其優勢在于能夠實作邏輯推理的完全自動化。
可滿足性模理論考慮的謂詞邏輯理論主要包括含有等于符号的未解釋函數(EUF)、位向量(BV)、數組(Array)、整數線性算術(LIA)、實數線性算術(LRA)、整數非線性算術(NIA)、字元串(String)等。求解SMT公式可滿足性問題的工具被稱為SMT求解器。目前，比較有代表性的SMT求解器有微軟開發的Z3求解器、美國斯坦福大學和愛荷華大學開發的CVC4/CVC5求解器、美國斯坦福國際研究院開發的Yices求解器等。對SMT求解的研究不但是自動推理、限制求解領域主流國際會議IJCAR/CADE、CP和SAT的主題，同時也是形式驗證和程式設計語言領域的重要國際會議CAV、POPL、FM、TACAS上非常活躍的議題。SMT同時也受到産業界的高度關注，微軟、英特爾、亞馬遜、Cadence等公司的研究院或實驗室都在開展與SMT相關的研究項目。
發展曆程：
實作邏輯推理自動化是人類社會的終極夢想之一，貫穿人類文明的發展曆程。20世紀50-60年代，人工智能的符号學派對于邏輯推理自動化進行了探讨，開發了一些邏輯推理系統[1,2,3,4]，但這些系統的推理能力普遍較弱。2000年左右，命題邏輯的可滿足性問題（SAT）求解取得突破，普林斯頓大學的Sharad Malik團隊開發了SAT求解器Chaff[5]，首次實作了對大規模命題邏輯公式的求解，并且開始應用于工業界解決實際問題。幾乎同時，各種特殊邏輯理論的判定算法的研究開始複興，出現了一批早期的求解器，比如斯坦福大學的SVC[6]和SteP[7]、SRI的ICS[8]等。研究人員随後考慮了SAT和特殊理論判定算法的融合，由此提出了可滿足性模理論問題(SMT)[9]。SMT發展的裡程碑包括：2003年開始組織每年一度的SMT研讨會(SMT Workshop)[10]、2004年提出了 SMT-LIB作為SMT問題求解的輸入格式标準[11]、2005年建立了SMT競賽(SMT-COMP)[12]。迄今為止，SMT競賽收集了超過100,000個測試用例。2010年之後出現了一批比較成熟的SMT求解器，比如美國微軟的Z3[13]、美國斯坦福大學和愛荷華大學的CVC4/ CVC5[14,15]、美國斯坦福國際研究院的Yices[16]等。
應用領域：
SMT求解器已經成為軟體工程、程式設計語言、以及資訊安全領域的基礎引擎，其應用場景多種多樣，下面對這些應用場景進行具體闡述。
軟體分析與驗證：
軟體演繹驗證歸結為兩個邏輯公式的蘊涵問題，然後可以編碼為SMT的可滿足性問題進行求解。微軟基于Z3求解器開發了程式演繹驗證工具Dafny[17]與Boogie[18]。
軟體的符号執行将路徑限制編碼為SMT公式，進而将路徑可行性問題編碼為SMT問題，如果SMT公式有解，則可以生成測試用例。斯坦福大學基于SMT求解器開發了符号執行工具Klee[19]，微軟基于Z3求解器開發了測試用例生成工具Pex[20]。
文法制導的程式合成問題基于程式模版生成程式，其基本思想是将程式合成問題編碼為SMT公式，利用SMT求解器來搜尋符合要求的程式[21]。
軟體模糊測試是近十年以來的一種非常流行的發現軟體系統漏洞的技術，基于動态執行的黑盒模糊測試存在覆寫率較低的問題，是以研究人員已經提出了白盒模糊測試，即将符号執行和動态執行相結合來尋找更多的漏洞，而SMT求解器是符号執行的核心，是以白盒模糊測試技術廣泛使用SMT求解器。微軟基于Z3求解器開發了模糊測試工具SAGE[22]，發現了Windows應用的很多漏洞。
定理證明：SMT求解器已經內建到了很多互動式定理證明器比如Coq和Isabelle中用于提升其自動化程度[23,24]。
雲計算安全性：亞馬遜Web服務建立了自動推理組, 基于SMT求解器開發了Zelkova工具和sideTrail工具，其中前者用于驗證AMS身份和密鑰管理政策以及簡單存儲服務配置政策的安全性，後者用于驗證密碼算法實作關于側信道攻擊的安全性[25]。
參考文獻：
[1] Allen Newell, Herbert A. Simon: The logic theory machine-A complex information processing system. IRE Trans. Inf. Theory 2(3): 61-79 (1956)
[2] Allen Newell, J. C. Shaw, Herbert A. Simon: Empirical explorations of the logic theory machine: a case study in heuristic. IRE-AIEE-ACM Computer Conference (Western) 1957: 218-230.
[3] Allen Newell, J. C. Shaw: Programming the logic theory machine. IRE-AIEE-ACM Computer Conference (Western) 1957: 230-240.
[4] John Alan Robinson: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12(1): 23-41 (1965)
[5] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: Chaff: Engineering an Efficient SAT Solver. DAC 2001: 530-535.
[6] Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt: A Decision Procedure for an Extensional Theory of Arrays. LICS 2001: 29-37.
[7] Zohar Manna, Nikolaj Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Luca de Alfaro, Harish Devarajan, Arjun Kapur, Jaejin Lee, Henny Sipma, Tomás E. Uribe: STeP: The Stanford Temporal Prover. TAPSOFT 1995: 793-794.
[8] Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar: ICS: Integrated Canonizer and Solver. CAV 2001: 246-249.
[9] Cesare Tinelli: A DPLL-Based Calculus for Ground Satisfiability Modulo Theories. JELIA 2002: 308-319.
[10] http://smt-workshop.cs.uiowa.edu/
[11] http://smtlib.cs.uiowa.edu/
[12] https://smt-comp.github.io/
[13] https://github.com/Z3Prover/z3
[14] https://cvc4.github.io/
[15] https://github.com/cvc5
[16] https://yices.csl.sri.com/
[17] https://github.com/dafny-lang/dafny
[18] https://github.com/boogie-org/boogie
[19] https://klee.github.io/
[20] http://duderino.github.io/injection/PexAndMoles.html
[21] https://sygus.org/
[22] Patrice Godefroid, Michael Y. Levin, David A. Molnar: Automated Whitebox Fuzz Testing. NDSS 2008.
[23] https://smtcoq.github.io/
[24] Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson: Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51(1): 109-128 (2013).
[25] https://aws.amazon.com/cn/blogs/security/tag/automated-reasoning/
術語工委及術語平台介紹：
計算機術語審定委員會(Committee on Terminology)主要職能為收集、翻譯、釋義、審定和推薦計算機新詞，并在CCF平台上宣傳推廣。這對厘清學科體系，開展科學研究，并将科學和知識在全社會廣泛傳播，都具有十分重要的意義。
術語衆包平台CCFpedia的建設和持續優化，可以有效推進中國計算機術語的收集、審定、規範和傳播工作，同時又能起到各領域規範化标準定制的推廣作用。
新版的CCFpedia計算機術語平台(http://term.ccf.org.cn)将術語的編輯營運與浏覽使用進行了整合，摒棄老版中跨平台操作的繁瑣步驟，在界面可觀性上進行了更新，讓使用者能夠簡單友善地查閱術語資訊。同時，新版平台中引入知識圖譜的方式對所有術語資料進行組織，通過圖譜多層關聯的形式更新了術語浏覽的應用形态。
計算機術語審定工作委員會
主任：
劉挺（哈爾濱工業大學）
副主任：
王昊奮（同濟大學）
李國良（清華大學）
主任助理：
李一斌（上海海乂知資訊科技有限公司）
執行委員：
丁軍（上海海乂知資訊科技有限公司）
林俊宇（中國科學院資訊工程研究所）
蘭豔豔（清華大學）
張偉男（哈爾濱工業大學）
