欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
Formal verification
来自开放百科 - 灰狐
(版本间的差异)
小 (→简介) |
小 (→语言) |
||
第28行: | 第28行: | ||
==语言== | ==语言== | ||
− | *[[Haskell]] [[Agda]] 具有“证明即程序、命题为类型”的特征。 | + | *[[Haskell]] [[Agda]] [[Idirs]] 具有“证明即程序、命题为类型”的特征。 |
*[[OCaml]] [[Coq]] | *[[OCaml]] [[Coq]] | ||
*[[ML]] [[isabelle]] | *[[ML]] [[isabelle]] |
2022年1月1日 (六) 12:54的版本
您可以在Wikipedia上了解到此条目的英文信息 Formal verification Thanks, Wikipedia. |
Proof assistant
目录 |
简介
“在科学的问题上,一千人的权威比不上一个人谦卑的推理。” ——伽利略
在数学、逻辑和计算机科学中,形式语言(Formal language)是用精确的数学或机器可处理的公式定义的语言。
这里指包含 Proof assistant 证明助理(证明助手) 在内的所有形式化相关主题,包含计算机辅助定理证明、Coq 证明助理、函数式编程、操作语义、用于论证软件的逻辑和技术、静态类型系统、基于性质的随机测试、以及对实践中编程代码的验证等。
在计算机科学和软件工程领域,形式化方法是使用适当的数学分析以提高设计的可靠性和强健性,适合于软件和硬件系统的描述、开发和验证。
形式验证(Formal verification)可以分为三大类:抽象解释(Abstract Interpretation)、形式模型检查(Formal Model Checking,也称作特性检查)和定理证明(Theory Prover)。
非形式化证明是算法,形式化证明是代码。
覆盖的核心概念有:
- 逻辑学中的基本工具,用于准确地提出并论证关于程序的假设,逻辑学被称之为计算机科学的微积分;
- 证明助理用于构造严谨的逻辑论据,分为两类:自动定理证明器和证明助理(如:Coq、Isabelle、Agda);
- 函数式编程思想,同时作为一种编程方法来简化程序的论证,以及架起程序和逻辑学之间的桥梁。
功能
指南
语言
- Haskell Agda Idirs 具有“证明即程序、命题为类型”的特征。
- 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
文档
- A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
- Isar — A language for structured proofs
图书
- 《Software Foundations》 软件基础系列是对可靠软件的数学基础的广泛介绍。该系列的主要创新之处在于,每一个细节都是百分之百的形式化和机器检查:每一卷的整个文本,包括练习,实际上是Coq证明助手的 "证明脚本"。
- 《软件基础》系列广泛地介绍了可靠软件的数学基础,这是《Software Foundations》中文版。
图集
链接
分享您的观点