Formal verification

2022年2月5日 (六) 02:41的版本

您可以在Wikipedia上了解到此条目的英文信息 Formal verification Thanks, Wikipedia.

Proof assistant

简介

Proof assistant, Theorem Prover, Formal verification, Hardware verification ...

Open Provable Foundation

“在科学的问题上，一千人的权威比不上一个人谦卑的推理。” ——伽利略

在数学、逻辑和计算机科学中，形式语言（Formal language）是用精确的数学或机器可处理的公式定义的语言。

这里指包含 Proof assistant 证明助理（证明助手）在内的所有形式化相关主题，包含计算机辅助定理证明、Coq 证明助理、函数式编程、操作语义、用于论证软件的逻辑和技术、静态类型系统、基于性质的随机测试、以及对实践中编程代码的验证等。

在计算机科学和软件工程领域，形式化方法是使用适当的数学分析以提高设计的可靠性和强健性，适合于软件和硬件系统的描述、开发和验证。

形式验证（Formal verification）可以分为三大类：抽象解释（Abstract Interpretation）、形式模型检查（Formal Model Checking，也称作特性检查）和定理证明（Theory Prover）。

非形式化证明是算法，形式化证明是代码。

覆盖的核心概念有：

逻辑学中的基本工具，用于准确地提出并论证关于程序的假设，逻辑学被称之为计算机科学的微积分；
证明助理用于构造严谨的逻辑论据，分为两类：自动定理证明器和证明助理（如：Coq、Isabelle、Agda）；
函数式编程思想，同时作为一种编程方法来简化程序的论证，以及架起程序和逻辑学之间的桥梁。

理论

形式科学是指主要研究对象为抽象形态的科学，如逻辑、数学、数理逻辑、信息论、统计学（数理统计学）、理论计算机科学（计算理论）、经济学（博弈论）等。

数理逻辑（Mathematical logic）是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。

证明论（又名元数学）是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。

形式（formal）语言是人工语言（constructed）的一种，是从特定的初始符号出发经过特定的形成规则所形成的语言，比如电报代码、计算机语言、数学语言、逻辑语言等。

功能

指南

语言

Haskell Agda Idris 具有“证明即程序、命题为类型”的特征。
OCaml Coq
ML isabelle
Lisp ACL2 Theorem Provers in Common Lisp
Racket cur

项目

Provably Awesome
Proof Assistant Open Source Projects on Github
proof assistant @ higithub
DeepSpec The Science of Deep Specification
Coq
Agda
Idris
ACL2
F* A Proof-oriented Programming Language
Prototype Verification System (PVS) 使用 Common Lisp 编写
hs-to-coq
Formal Verification of Ethereum Contracts Ethereum
HOL Interactive Theorem Prover
HACL* a formally verified cryptographic library（形式化验证密码学库）written in F*
Dafny is a verification-aware programming language 使用 C# 编写，采用 MIT 许可证。
Programming with Refinement Types An Introduction to LiquidHaskell
isabelle is a generic proof assistant Isabelle 形式化证明存档（Archive of Formal Proofs）
The Little Prover
Proof General Organize your proofs!
The red* family of proof assistants
The Principia Rewrite 《数学原理》重写工程——该项目致力于将罗素与怀特海的《数学原理》使用 Coq 语言完全重写，补全原书的逻辑漏洞，将其中的证明进行 100% 的机器形式化验证。同时，项目还会将 Coq 的证明进行排版，生成和原书风格一致、可检索、排版精致的文本供人类阅读。@Libre盖子

STEM

Iris Project Lecture Notes Iris: Higher-Order Concurrent Separation Logic

文档

图书

《Software Foundations》软件基础系列是对可靠软件的数学基础的广泛介绍。该系列的主要创新之处在于，每一个细节都是百分之百的形式化和机器检查：每一卷的整个文本，包括练习，实际上是Coq证明助手的 "证明脚本"。
《软件基础》系列广泛地介绍了可靠软件的数学基础，这是《Software Foundations》中文版。
《芯片验证漫游指南：从系统理论到UVM的验证全视界》刘斌

数字集成系统的验证，是提高设计芯片一次流片成功的关键。随着芯片制造工艺的更加精细，芯片制造费用的不断增加，芯片功能越来越复杂，验证的重要性也日益增加。