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：量子密码学的形式验证
使用形式化方法进行语言细化