plt formal methods resources下載 - plt formal methods resources原始碼下載

plt formal methods resources

其他源碼

1.0.0

下載

程式語言理論與形式化方法 - 資源

圖片來源：福賽集團

形式化方法是用於設計、驗證和規範軟體和硬體問題的數學技術。這些本質上是程式語言理論研究的一個子集，用於研究複雜的電腦科學問題。

形式化方法分析基本上涉及以下步驟：

Formal Specification
Formal Proofs
Model Checking
Abstraction

形式證明開發和模型檢查主要使用互動式定理證明器（通常稱為證明助手）來完成。抽像是在模型各部分之間創造結構上合理的關係。

這是我嘗試整理的一系列有用的閱讀材料、影片和工具，以及該領域即將面臨的一些挑戰。

筆記：

我試著讓內容更加關注目前的研究和工業應用。尋找純粹學術收藏的人必須參考《正式教育方法》——傑里米·阿維加德 (Jeremy Avigad)。
希望讀者俱備類型理論的一些基本知識。更多學術見解可以在這裡找到 learn-tt。

內容

書籍和講座
部落格
慕課
工具
專案
即將到來的挑戰
- 安全相關
  - 軟體安全
  - 差異隱私
  - 區塊鏈安全中的應用
  - 確保人工智慧安全的挑戰
  - 建立安全的網路實體系統
- 著重抽象解釋
- 程式語言研究相關
  - 機率規劃
  - 量子程式語言的發展
  - 使用形式化方法進行語言細化
相關產業和新創公司

書籍和講座

軟體基礎：我強烈建議將此作為深入研究該領域的起始材料。這本書對於建立基本概念非常有幫助，並且是對該領域的非常完善的介紹。整個過程中提供了精美插圖的概念和練習範例，使互動式定理證明學習變得有趣。
FRAP - Adam Chlipala ：一本幫助您理解和推理程序形式正確性的書。命令式語言（ C ）啟發的資料結構和演算法範例極大地幫助我們開始思考它們的形式驗證。
Certified Programming with Dependent Types - Adam Chlipala ：使用 coq 學習定理證明的最佳theoretical books之一。
形式驗證 - Jacques Fleuriot ：這門課程涉及使用一些更發達的工具（如 SAT 和 SMT 求解器）進行定理證明。
抽象解釋 - Patrick Cousot有關抽象解釋理論的最佳可用資料。它給出了程序突變的完整而純粹的數學分析。程序行為作為不同抽象數學結構之間不斷修改的關係得到了解釋和證明！
邏輯與證明 - CMU 與精實簡介：這是在 CMU 設計的課程，也可作為精實定理證明的入門資料

如果您覺得需要更多理論見解，請參閱上面的註釋。

部落格

正式方法入門
K 框架和區塊鏈形式化驗證的努力
Pact Formal Verification for Blockchain smart Contract：很棒的簡短博客，解釋了Pact FV 的方法，並簡要介紹了第一原理的形式驗證。
邁向穩健且經過驗證的人工智慧：規格測試、穩健訓練和形式驗證 - DeepMind
機器學習驗證和測試的挑戰 - Ian GoodFellow 和 Nicolas Papernot

慕課

正式軟體驗證 - edX
定量模型檢查 - Coursera
網路物理系統：加州大學柏克萊分校的課程，重點是使用驗證方法對網路物理系統（CPS）進行建模。
程式語言 - Coursera

工具

證明助理

coq：最受歡迎和最廣泛使用的定理證明器。它支援許多功能，包括 ML 提取、專案打包（專案和 Makefile 創建）。有大量使用 coq 進行形式化的how-to材料。任何人都可能會發現 Coq 中的 100 個定理非常有趣。
精實：微軟研究院的一個相當新的定理證明器。有一個很好的互動式教程，很容易上手。
PRISM模型檢查器：它是由牛津大學開發的模型檢查器。
Nuprl：康乃爾大學證明細化邏輯計畫下的定理證明器。
Agda：相當成熟的證明助手。具有與 Coq 類似的功能。經過一些 coq 經驗後很容易學習。
伊莎貝爾：這是一個古老的定理證明者。具有很好的核心邏輯實現，但缺乏其他與使用者體驗相關的功能。
VCC：Microsoft 的並發 C 程式的機械驗證器。
TLA+：用於建模語言和系統的高階語言（尤其是並發和分散式）。

SAT/SMT/SMC 求解器

SAT 求解器：

迷你衛星。

SMT 求解器：

Z3
CVC4
數學SAT5
SMT國際刑警組織
公主

SMC 求解器：

出版品

混合求解器

證明助手對程式邏輯有非常強大的實作。有時僅通過使用它們來進行複雜的證明在戰術上可能是不可能的。因此，目前的研究將這種基於強邏輯的推理原理與強大的 SMT 和 SMC 求解器相結合，以簡化證明開發。下面是一些範例：

F星(F*)
- 可以使用 KreMLin 將 F* 程式碼提取為 C。
SMTCoq

專案

大多數專案或多或少都是各自定理證明器或 SAT/SMT/SMC/求解器的開發，因此可以在那裡找到。這些是積極開發的其他一些項目。

DeepSpec 是一個傘式項目，專注於建立經過驗證的軟體系統。正在積極進行以下主要子項目：
- 電腦證書
- 已驗證的 LLVM (VeLLVM)
- 已驗證的軟體工具鏈 (VST)
ikos 是一個基於抽象解釋理論的可靠、無錯誤的C 編譯器。
Project Everest：這是一個旨在創建安全且經過驗證的 HTTPS 生態系統的研究計畫。
CertiCrypt：這是一個專注於使用 coq 證明助手對公鑰加密進行建模的專案。
Iris：Iris 是一個在證明助手 Coq 中實現和驗證的高階並發分離邏輯框架。
VeriDeep - 深度神經網路的安全驗證
VeHICal：專案重點是為人類網路物理系統的介面和控制的經過驗證的協同設計奠定基礎。
FastSMT - 透過學習最佳化公式資料集效能來增強 SMT 求解器的工具。它由蘇黎世聯邦理工學院 SRI 實驗室開發，基於 Z3 SMT 求解器。
fm4cps - 資訊物理系統的形式化方法，INRIA 和華東師範大學上海分校共同努力。

即將到來的挑戰

安全相關

軟體安全
- 讀物
  - 安全正式方法，NSF 研討會
  - 形式方法與安全性之間的符號關係
  - 珠穆朗瑪峰研究論文項目
  - 軟體安全中的形式化方法
  - 安全可靠的電腦系統的形式化方法
  - 形式加密的計算可靠性
  - 使用形式化方法的安全結構
  - 密碼原語驗證
  - 基於遊戲的密碼證明的正式認證
  - 基於代碼的密碼證明的正式認證
- 影片
  - Dropbox 的深度規範
  - 用於 F* 中經過驗證的安全多方計算的 DSL
  - 使用形式化方法開發高度安全的系統
  - 透過形式方法和安全架構實現安全性（CERIAS - 普渡大學）
  - 基於語言的密碼學和隱私技術
差異隱私
- 讀物
  - 互動式系統差分隱私的形式化驗證
  - 保護隱私的正式方法
  - LightDP - 邁向自動化差異隱私證明
  - EasyCrypt - 經驗證的計算差分隱私與智慧電錶的應用
  - 在霍爾邏輯中證明差分隱私
  - 差分私有貝葉斯規劃
  - 差分隱私的高階機率耦合
- 影片
  - 隱私屬性的形式化方法和證明 - 1
  - 隱私屬性的形式化方法和證明 - 2
  - 隱私屬性的形式化方法和證明 - 3
  - 使用關係類型證明差異隱私
區塊鏈安全中的應用
區塊鏈的形式化方法：這是有史以來第一個專注於在區塊鏈技術中使用形式化方法的研討會。日期為2019 年 10 月 11 日。
CertiK ：這是一家專注於使用正式方法使區塊鏈可驗證安全的新創公司。
- 讀物
  - 形式分析和驗證如何為基於區塊鏈的系統添加安全性 - 麻省理工學院教程
  - 智能合約和正式方法的機會
  - K 框架和區塊鏈中形式驗證的努力關於 K 框架及其在驗證區塊鏈系統中的應用的解釋材料的精彩集合。
  - Pact Formal Verification for Blockchain smart Contract：很棒的簡短博客，解釋了Pact FV 的方法，並簡要介紹了第一原理的形式驗證。
  - 時態區塊鏈 - 正式分析
  - 透過博弈論和形式化方法驗證去中心化智能合約
- 影片
  - 區塊鏈語言的形式化設計、實作與驗證
  - CertiK - 智慧合約形式化驗證平台（回顧）
  - 簡單性—區塊鏈的新語言
確保人工智慧安全的挑戰
FLoC 2018-機器學習高峰會遇見形式化方法
驗證機器學習 - Radboud University Nijmegen ：關於在機器學習中使用驗證方法的大學課程。
形式化方法與機器學習的結合 - 亞琛工業大學：2018 年關於使用形式化方法實現可驗證安全機器學習進展的研討會。
- 讀物
  - 邁向經過驗證的人工智慧 - S. Seshia
  - 邁向穩健且經過驗證的人工智慧：規格測試、穩健訓練和形式驗證 - DeepMind
  - 使用形式數學開發無錯誤的機器學習系統
  - 混合形式方法、機器學習和人機交互
  - 形式化方法中的機器學習
  - 機器學習和形式化方法
  - 驗證深度神經網路的演算法
  - 深度神經網路的安全驗證
  - 機器學習驗證和測試的挑戰 - Ian GoodFellow 和 Nicolas Papernot
  - 驗證二值化深度神經網路的屬性
  - Reluplex：用於驗證深度神經網路的高效能 SMT 求解器
  - 分段線性前饋網路的驗證
  - 強化學習演算法驗證的挑戰
  - 在強化學習中應用形式化方法 - Galois Inc.
  - 證明深度神經網路的對抗穩健性
- 影片
  - 深度神經網路安全驗證 -ICST 2018
  - 深度神經網路的安全驗證 - Marta Kwiatkowska - CAV 2017
  - 深度神經網路的安全驗證-INRIA
  - 機器學習驗證規則，從數據驅動的錯誤到可解釋的人工智慧
  - 機器學習程序的驗證
  - Reluplex：用於驗證深度神經網路的高效 SMT 求解器 - 會議視頻
  - 使用 Certigrad 開發無錯誤的機器學習模型 - Daniel Selsam
建立安全的網路實體系統
VeHICal ：專案重點是為人類網路物理系統的介面和控制的經過驗證的協同設計奠定基礎。
fm4cps - 資訊物理系統的形式化方法，INRIA 和華東師範大學上海分校共同努力。
- 讀物
  - 資訊物理系統設計：形式基礎、方法與整合工具鏈
  - 形式化方法的新領域：學習、網路物理系統、教育等
  - 資訊物理系統的統計模型檢查
  - 交通資訊物理系統的形式驗證
  - 資訊物理系統的驗證
  - 網路物理系統的驗證和驗證：研究挑戰和前進方向
  - 網路物理系統中的異常檢測：形式化方法
  - 自適應資訊物理系統的組成驗證
- 影片
  - 網路物理系統和工業物聯網的正式方法憲章
  - 網路物理系統的形式驗證
  - 監控網路實體系統

著重抽象解釋

快速有效的穩健性認證：DeepZ 計畫 - 用於基於抽象解釋來認證神經網路的穩健性。
AI2：具有抽象解釋的神經網路的安全性和穩健性認證
提高神經網路的穩健性認證：在其方法中使用抽象解釋。

程式語言研究相關

機率規劃
- 讀物
  - 機率規劃簡介
  - 高階機率程序的形式驗證
  - 機率邏輯程式設計和貝葉斯網絡
  - 高階邏輯中的機率函數和密碼學預言 - Andreas Lochbihler
  - 密碼實現的機率關係驗證
  - 耦合證明是機率產物程序
  - 差分隱私的高階機率耦合
  - 機率規劃的形式化方法
  - 機率程序的形式化方法：講授幻燈片
  - 機率編程 - 真實驗證挑戰
  - FairSquare：程式公平性的機率驗證
  - VPHL：經過驗證的機率程序的部分正確性邏輯
  - 統一邏輯與機率
- 影片
  - 高階機率程序的形式化驗證 - POPL 2019 會議視頻
  - 機率邏輯程式設計及其應用 - Luc De Raedt，魯汶
量子程式語言的發展
- 讀物
  - Qwire：Coq 中量子程式的形式驗證
  - 量子程序形式化驗證的邏輯
  - 量子程序推理的耦合技術
  - 形式驗證與量子不確定性
  - 模型檢查遞歸量子協議
- 影片
  - 用於軟體驗證和驗證 (VV) 的任務能力量子計算 - CMU
  - Dominique Unruh：量子密碼學的形式驗證
使用形式化方法進行語言細化