Formal verification

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(语言)
(语言)
(未显示1个用户的31个中间版本)
第4行: 第4行:
  
 
==简介==
 
==简介==
 +
“在科学的问题上,一千人的权威比不上一个人谦卑的推理。” ——伽利略
 +
 +
[[Open Provable Foundation]]
 +
 
Formal verification, Proof assistant, Theorem Prover, Software verification, Hardware verification ...
 
Formal verification, Proof assistant, Theorem Prover, Software verification, Hardware verification ...
  
第9行: 第13行:
  
 
形式验证可以分为三大类:抽象解释(Abstract Interpretation)、形式模型检查(Formal Model Checking,也被称作特性检查)和理论验证器(Theory Prover)。  
 
形式验证可以分为三大类:抽象解释(Abstract Interpretation)、形式模型检查(Formal Model Checking,也被称作特性检查)和理论验证器(Theory Prover)。  
 
[[Open Provable Foundation]]
 
 
“在科学的问题上,一千人的权威比不上一个人谦卑的推理。” ——伽利略
 
  
 
这里指包含 Proof assistant 证明助理(证明助手) 在内的所有形式化相关主题,包含计算机辅助定理证明、[[Coq]] 证明助理、函数式编程、操作语义、用于论证软件的逻辑和技术、静态类型系统、基于性质的随机测试、以及对实践中编程代码的验证等。
 
这里指包含 Proof assistant 证明助理(证明助手) 在内的所有形式化相关主题,包含计算机辅助定理证明、[[Coq]] 证明助理、函数式编程、操作语义、用于论证软件的逻辑和技术、静态类型系统、基于性质的随机测试、以及对实践中编程代码的验证等。
第23行: 第23行:
 
*Verification 验证表明的是满足规定要求。
 
*Verification 验证表明的是满足规定要求。
 
*Validation 确认就是检查最终产品是否达到顾客使用要求。
 
*Validation 确认就是检查最终产品是否达到顾客使用要求。
 +
参考
 +
*[https://www.ni.com/zh-cn/innovations/electronics/automated-design-validation-and-verification.html Automated Design Validation and Verification (V&V)]
  
 
==理论==
 
==理论==
第39行: 第41行:
  
 
*[https://en.wikipedia.org/wiki/Formal_system Formal system] 形式系统 [https://en.wikipedia.org/wiki/Formal_language Formal language] 形式语言 [https://en.wikipedia.org/wiki/Formal_grammar Formal grammar] 形式文法
 
*[https://en.wikipedia.org/wiki/Formal_system Formal system] 形式系统 [https://en.wikipedia.org/wiki/Formal_language Formal language] 形式语言 [https://en.wikipedia.org/wiki/Formal_grammar Formal grammar] 形式文法
*[https://en.wikipedia.org/wiki/Satisfiability_modulo_theories satisfiability modulo theories (SMT)] 可满足性修改理论 [https://smt-comp.github.io/ SMT-COMP]
+
*[https://en.wikipedia.org/wiki/Satisfiability_modulo_theories satisfiability modulo theories (SMT)] 可满足性模理论 [https://smt-comp.github.io/ SMT-COMP] [https://leodemoura.github.io/files/mpi2009.pdf SMT @ Microsoft]
 
*[https://en.wikipedia.org/wiki/Automated_theorem_proving Automated theorem proving (ATP)] 自动化定理证明
 
*[https://en.wikipedia.org/wiki/Automated_theorem_proving Automated theorem proving (ATP)] 自动化定理证明
 
*[https://en.wikipedia.org/wiki/First-order_logic First-order logic] 一阶逻辑
 
*[https://en.wikipedia.org/wiki/First-order_logic First-order logic] 一阶逻辑
第64行: 第66行:
  
 
==语言==
 
==语言==
 +
[[文件:purely-functional-programming.png]]
 +
*在数学、逻辑和计算机科学中,形式语言([https://en.wikipedia.org/wiki/Formal_language Formal language])是用精确的数学或机器可处理的公式定义的语言。
 
*[[F*]]
 
*[[F*]]
*[[Haskell]] [[Agda]] [[Idris]] 具有“证明即程序、命题为类型”的特征。[https://github.com/plclub/hs-to-coq hs-to-coq] import [[Haskell]] to Coq
+
*[[Haskell]] [[Agda]] [[Idris]] 具有“证明即程序、命题为类型”的特征。[https://github.com/plclub/hs-to-coq hs-to-coq] import [[Haskell]] to Coq, [https://github.com/nick8325/jukebox/ jukebox] A theorem prover
 
*[[OCaml]] [[Coq]] [https://github.com/formal-land/coq-of-ocaml coq-of-ocaml] 可做两件事:1、do formal proofs on OCaml programs; 2、port OCaml projects to Coq.
 
*[[OCaml]] [[Coq]] [https://github.com/formal-land/coq-of-ocaml coq-of-ocaml] 可做两件事:1、do formal proofs on OCaml programs; 2、port OCaml projects to Coq.
*[[ML]] [[isabelle]]
+
*[[ML]] [[isabelle]] [https://cakeml.org/ CakeML] A Verified Implementation of ML
*[[Lisp]] [[ACL2]] [https://www.cliki.net/Theorem%20Provers Theorem Provers in Common Lisp]
+
*[[Lisp]] [[ACL2]] [https://pvs.csl.sri.com/ PVS] [https://www.cliki.net/Theorem%20Provers Theorem Provers in Common Lisp]
 
*[[Racket]] [https://github.com/wilbowma/cur cur]
 
*[[Racket]] [https://github.com/wilbowma/cur cur]
 
*[[Common Lisp]] [http://www.nuprl.org/ PRL Project] Proofs as Programs
 
*[[Common Lisp]] [http://www.nuprl.org/ PRL Project] Proofs as Programs
 
*[https://github.com/leanprover Lean] Prover
 
*[https://github.com/leanprover Lean] Prover
 
*[http://smtlib.cs.uiowa.edu/language.shtml SMT-LIB Language] 包含三大组件:theory declarations, logic declarations, and scripts
 
*[http://smtlib.cs.uiowa.edu/language.shtml SMT-LIB Language] 包含三大组件:theory declarations, logic declarations, and scripts
 +
*[[Hardware description language]] for Formal verification
  
 
==项目==
 
==项目==
 
[[文件:Coq-logo.png|right|Coq]]
 
[[文件:Coq-logo.png|right|Coq]]
 +
[[文件:z3-logo.png|right|Z3]]
 
[[文件:Isabelle-logo.gif|right|isabelle]]
 
[[文件:Isabelle-logo.gif|right|isabelle]]
 
[[文件:Lean-logo.png|right|Lean]]
 
[[文件:Lean-logo.png|right|Lean]]
第81行: 第87行:
 
[[文件:deepspec-logo.png|right]]
 
[[文件:deepspec-logo.png|right]]
 
[[文件:vellvm-logo.jpg|right|Vellvm]]
 
[[文件:vellvm-logo.jpg|right|Vellvm]]
 +
[[文件:key-logo.png|right|KeY]]
 
*[https://github.com/awesomo4000/awesome-provable Provably Awesome] [[文件:awesome.png]]  
 
*[https://github.com/awesomo4000/awesome-provable Provably Awesome] [[文件:awesome.png]]  
 
*[https://awesomeopensource.com/projects/proof-assistant Proof Assistant Open Source Projects on Github]
 
*[https://awesomeopensource.com/projects/proof-assistant Proof Assistant Open Source Projects on Github]
第91行: 第98行:
 
*[[Idris]]
 
*[[Idris]]
 
*[[ACL2]]
 
*[[ACL2]]
 +
*[[Z3|Z3 Theorem Prover]] [https://theory.stanford.edu/~nikolaj/programmingz3.html Programming Z3]
 
*[[F*]] A Proof-oriented Programming Language
 
*[[F*]] A Proof-oriented Programming Language
*[https://yices.csl.sri.com/ Yices]
 
*[https://github.com/z3prover/z3 Z3] [https://theory.stanford.edu/~nikolaj/programmingz3.html Programming Z3]
 
 
*[https://cvc4.github.io/ CVC4]
 
*[https://cvc4.github.io/ CVC4]
*[https://pvs.csl.sri.com/ Prototype Verification System (PVS)] [https://github.com/SRI-CSL/PVS PVS Specification and Verification System] written in [[Common Lisp]]
+
*[https://github.com/SRI-CSL SRI International's Computer Science Laboratory] [https://github.com/SRI-CSL/yices2 Yices SMT Solver] [https://pvs.csl.sri.com/ Prototype Verification System (PVS)] [https://github.com/SRI-CSL/PVS PVS] [https://github.com/nasa/pvslib NASALib] written in [[Common Lisp]]
*[https://sri-csl.github.io/ SRI International - Computer Science Laboratory]
+
*[https://github.com/SRI-CSL/PVS Prototype Verification System (PVS)] 使用 [[Common Lisp]] 编写
+
 
*[https://github.com/plclub/hs-to-coq hs-to-coq]
 
*[https://github.com/plclub/hs-to-coq hs-to-coq]
 
*[https://github.com/pirapira/ethereum-formal-verification-overview Formal Verification of Ethereum Contracts] [[Ethereum]]
 
*[https://github.com/pirapira/ethereum-formal-verification-overview Formal Verification of Ethereum Contracts] [[Ethereum]]
第123行: 第127行:
 
*[https://github.com/sifive/Kami Kami] — A [[Coq]]-based [[DSL]] for specifying and proving hardware designs
 
*[https://github.com/sifive/Kami Kami] — A [[Coq]]-based [[DSL]] for specifying and proving hardware designs
 
*[https://github.com/sifive/RiscvSpecFormal RiscvSpecFormal] Formal Specification of [[RISC]]-V ISA in Kami, written in [[Haskell]].
 
*[https://github.com/sifive/RiscvSpecFormal RiscvSpecFormal] Formal Specification of [[RISC]]-V ISA in Kami, written in [[Haskell]].
 +
*[https://www.key-project.org/ KeY Project]
 +
*[https://www.tptp.org/ TPTP (Thousands of Problems for Theorem Provers)]
  
 
==STEM==
 
==STEM==
 +
*[https://fm.csl.sri.com/SSFT14/index.shtml Fourth Summer School on Formal Techniques]
 
*[https://iris-project.org/tutorial-material.html Iris Project Lecture Notes] Iris: Higher-Order Concurrent Separation Logic
 
*[https://iris-project.org/tutorial-material.html Iris Project Lecture Notes] Iris: Higher-Order Concurrent Separation Logic
  
 
==研究组织==
 
==研究组织==
 
[[文件:Automated-Reasoning.jpg|right|Automated Reasoning Group]]
 
[[文件:Automated-Reasoning.jpg|right|Automated Reasoning Group]]
 +
[[文件:nasa-fm-logo.jpg|right|NASA Langley's Formal Methods]]
 
*[https://flint.cs.yale.edu/ Yale FLINT group]
 
*[https://flint.cs.yale.edu/ Yale FLINT group]
 
*[http://verify.inf.usi.ch/ Formal Verification and Security Lab]
 
*[http://verify.inf.usi.ch/ Formal Verification and Security Lab]
第135行: 第143行:
 
*[https://toccata.gitlabpages.inria.fr/toccata/index.en.html Toccata] Formally Verified Programs, Certified Tools and Numerical Computation
 
*[https://toccata.gitlabpages.inria.fr/toccata/index.en.html Toccata] Formally Verified Programs, Certified Tools and Numerical Computation
 
*[https://plv.csail.mit.edu/ MIT Programming Languages & Verification Group]
 
*[https://plv.csail.mit.edu/ MIT Programming Languages & Verification Group]
 +
*[https://shemesh.larc.nasa.gov/fm/ NASA Langley Formal Methods Research Program]
 +
*[https://formalverification.cs.utah.edu/ FORMAL VERIFICATION AT UTAH]
  
 
==文档==
 
==文档==
第141行: 第151行:
 
*[https://daejunpark.github.io/deposit.pdf End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract]
 
*[https://daejunpark.github.io/deposit.pdf End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract]
 
*[https://flint.cs.yale.edu/flint/publications/feng-thesis.pdf An Open Framework for Certified System Software] [http://flint.cs.yale.edu/flint/publications/feng-thesis.html Author]
 
*[https://flint.cs.yale.edu/flint/publications/feng-thesis.pdf An Open Framework for Certified System Software] [http://flint.cs.yale.edu/flint/publications/feng-thesis.html Author]
 +
*[https://hol-theorem-prover.org/hol-course.pdf Interactive Theorem Proving (ITP) Course]
 +
*[https://fm.csl.sri.com/SSFT14/speaklogicV3.pdf Speaking Logic]
 +
*[https://fm.csl.sri.com/SSFT14/rosette-lecture.pdf Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond]
  
 
==图书==
 
==图书==
第169行: 第182行:
 
image:Automated-Formal-Verification.png|Automated Formal Verification
 
image:Automated-Formal-Verification.png|Automated Formal Verification
 
image:hifrog-architecture.png|HiFrog
 
image:hifrog-architecture.png|HiFrog
 +
image:KeY-Architecture.png|KeY架构
 +
image:KeY-JML.png|KeY & JML
 +
image:KeY-Symbolic-Execution-Debugger-SED.png|KeY SED
 +
image:Formal-verification-VLSI-design.png|VLSI设计形式化验证
 
</gallery>
 
</gallery>
  
第179行: 第196行:
 
*[https://bedrocksystems.com/ BedRock Systems] Unbreakable Foundation for Formally Secured Computing, [https://github.com/udosteinberg/NOVA NOVA] is the foundation for the BedRock HyperVisor(BHV), which combines a formally verified secure trusted computing base with VM introspection and policy enforcement.  
 
*[https://bedrocksystems.com/ BedRock Systems] Unbreakable Foundation for Formally Secured Computing, [https://github.com/udosteinberg/NOVA NOVA] is the foundation for the BedRock HyperVisor(BHV), which combines a formally verified secure trusted computing base with VM introspection and policy enforcement.  
 
*[https://www.sifive.com/ SiFive] rapid development of custom hardware solutions, based on [[RISC]]-V, Securing The RISC‑V Revolution.
 
*[https://www.sifive.com/ SiFive] rapid development of custom hardware solutions, based on [[RISC]]-V, Securing The RISC‑V Revolution.
 +
*[https://www.synopsys.com/verification.html Scalable SoC Verification] [https://www.synopsys.com/zh-cn/verification.html 可扩展的 SoC 验证,提前启动软件系统验证]
 +
*[https://www.cadence.com/zh_CN/home/tools/system-design-and-verification.html Cadence Verification]
 +
*[https://smt-comp.github.io/ International Satisfiability Modulo Theories Competition (SMT-COMP)] 国际可满足性模理论竞赛
  
 
[[category:formal]]
 
[[category:formal]]

2022年6月24日 (五) 09:01的版本

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

Formal verification

目录

简介

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

Open Provable Foundation

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

形式验证的含义是根据某个或某些形式规范或属性,使用数学的方法证明其正确性或非正确性。

形式验证可以分为三大类:抽象解释(Abstract Interpretation)、形式模型检查(Formal Model Checking,也被称作特性检查)和理论验证器(Theory Prover)。

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

新闻

V & V

验证(Verification)与确认(Validation)

  • Verification 验证表明的是满足规定要求。
  • Validation 确认就是检查最终产品是否达到顾客使用要求。

参考

理论

Metamath

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

Metamath 是用来发展严格形式化数学定义及证明的一款语言,亦指用来验证该语言的证明验证器,以及存有逻辑、集合论、数论、群论、代数、数学分析、拓扑学、希尔伯特空间及量子逻辑等领域中数万条已证明定理且仍不断在增加中的数据库。灰狐镜像

形式逻辑有传统与现代(即数理逻辑)之分,简单地说,形式逻辑是研究思维的形式及其规律的。

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

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

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

指南

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

在计算机科学和数理逻辑中,证明助手或交互式定理检验器是一种软件工具,通过人机协作来协助开发形式证明。

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

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

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

Formal-Verification.png DeepSpec The Science of Deep Specification

覆盖的核心概念有:

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

语言

Purely-functional-programming.png

项目

Coq
Z3
isabelle
Lean
ACL2
Deepspec-logo.png
Vellvm
KeY

STEM

研究组织

Automated Reasoning Group
NASA Langley's Formal Methods

文档

图书

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

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

图集

链接

Runtime Verification
bluespec
分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱