Formal verification

来自开放百科 - 灰狐
（版本间的差异）
跳转到： 导航, 搜索
小 (→‎图集)
小 (→‎语言)
 
（未显示1个用户的163个中间版本）
第1行： 第1行：
 
{{SeeWikipedia}}
 
{{SeeWikipedia}}
  
−
Proof assistant
+
Formal verification
  
 
==简介==
 
==简介==
 +
“在科学的问题上，一千人的权威比不上一个人谦卑的推理。” ——伽利略
 +
 +
[[Open Provable Foundation]]
 +
 +
Formal verification, Proof assistant, Theorem Prover, Software verification, Hardware verification ...
 +
 +
形式化方法是一种特别的基于数学的技术，用于软件和硬件系统的形式规范、开发以及验证。
 +
 +
形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。
 +
 +
形式验证可以分为三大类：抽象解释（Abstract Interpretation）、形式模型检查（Formal Model Checking，也被称作特性检查）和定理证明（Theory Prover）。
 +
 +
自动化定理证明（Automated theorem proving，ATP）目前是自动推理（Automated reasoning，AR）体系中发展最好的部分，它的目的是为使用电子计算机程序来进行数学定理的证明。对于不同的公理系统，它能够推论出一个定理在此系统下是正确的，还是不可证明的，或者错误的。
 +
 
这里指包含 Proof assistant 证明助理（证明助手） 在内的所有形式化相关主题，包含计算机辅助定理证明、[[Coq]] 证明助理、函数式编程、操作语义、用于论证软件的逻辑和技术、静态类型系统、基于性质的随机测试、以及对实践中编程代码的验证等。
 
这里指包含 Proof assistant 证明助理（证明助手） 在内的所有形式化相关主题，包含计算机辅助定理证明、[[Coq]] 证明助理、函数式编程、操作语义、用于论证软件的逻辑和技术、静态类型系统、基于性质的随机测试、以及对实践中编程代码的验证等。
 +
 +
==机器证明==
 +
 +
笛卡尔曾有过一个宏伟的设想：”一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。“他把问题问题想得过于简单了。如果他的设想真能实现，那就不仅是数学的机械化，而且是全部科学的机械化。因为，代数求解是可以机械化的。但笛卡尔没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座划时代的桥梁，实现了初等几何问题代数化。这为后来的几何定理机器证明的代数方法打下了基础。p.21
 +
 +
1977年，吴文俊提出的定理机器证明新方法正式发表。使用这新方法（简称吴法），可以在微机上迅速地证明很不简单的几何定理，如西姆松定理、费尔哈定理、莫勒定理等等；还能发现新的不平凡的的几何定理。1989年，访美学者周咸青基于吴法编制的 Lisp 程序（所谓”证明器“）在计算机上证明了512条定理。这些定理大多是不平凡的，其中还有新定理。证明每条定理所用的机器时间一般才几秒钟。p.27-28
 +
 +
《王者之路 机器证明及其应用》吴文俊等
 +
 +
吴氏方法的基本思想是，先把几何问题化为代数问题，再把代数问题化为代数恒等式的检验问题。代数恒等式的检验是机械的，问题的转化过程也是机械的，整个问题也就机械化了。《数学与哲学》张景中，p.156
 +
 +
==新闻==
 +
*[http://mp.weixin.qq.com/s?__biz=MzI4NTg4NzA3Mg==&mid=2247484718&idx=1&sn=73dc35b9d6f5c12787dafda1f8d00228&chksm=ebe41a21dc939337ff6f53e29cc44609a6c0298e5ff8907ee183d774faa11b5e06b08b9a2f84&scene=21#wechat_redirect 2018 年 9 月，Maker 协议成为首个通过形式化验证的去中心化协议] [https://github.com/dapphub/k-dss formal verification of multicollateral dai in the K framework]
 +
 +
==V & V==
 +
验证（Verification）与确认（Validation）
 +
*Verification 验证表明的是满足规定要求。
 +
*Validation 确认就是检查最终产品是否达到顾客使用要求。
 +
参考
 +
*[https://www.ni.com/zh-cn/innovations/electronics/automated-design-validation-and-verification.html Automated Design Validation and Verification (V&V)]
 +
 +
==理论==
 +
[[文件:metamath-logo.png|right|Metamath]]
 +
形式科学是指主要研究对象为抽象形态的科学，如逻辑、数学、数理逻辑、信息论、统计学（数理统计学）、理论计算机科学（计算理论）、经济学（博弈论）等。
 +
 +
[http://us.metamath.org/mm.html Metamath] 是用来发展严格形式化数学定义及证明的一款语言，亦指用来验证该语言的证明验证器，以及存有逻辑、集合论、数论、群论、代数、数学分析、拓扑学、希尔伯特空间及量子逻辑等领域中数万条已证明定理且仍不断在增加中的数据库。[https://docs.huihoo.com/proof/metamath.org/ 灰狐镜像]
 +
 +
形式逻辑有传统与现代（即数理逻辑）之分，简单地说，形式逻辑是研究思维的形式及其规律的。
 +
 +
[[数理逻辑]]（Mathematical logic）是数学的一个分支，其研究对象是对'''证明'''和'''计算'''这两个直观概念进行符号化以后的形式系统。数理逻辑是'''数学基础'''的一个不可缺少的组成部分。
 +
 +
证明论（又名元数学）是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和'''模型论'''，'''公理化集合论'''，以及'''递归论'''一起，'''证明论'''被称为数学基础的四大支柱之一。
 +
 +
形式（formal）语言是人工语言（constructed）的一种，是从特定的初始符号出发经过特定的形成规则所形成的语言，比如电报代码、计算机语言、数学语言、逻辑语言等。
 +
 +
*[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://leodemoura.github.io/files/mpi2009.pdf SMT @ Microsoft] [https://fm.csl.sri.com/SSFT22/piskac-lectures01.pdf SMT-based Verification of Heap-manipulating Programs] [https://fm.csl.sri.com/SSFT22/lecture2-new.pdf New update]
 +
*[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/Theory_of_pure_equality Theory of pure equality] 纯粹的平等理论
 +
*[https://en.wikipedia.org/wiki/Category:Systems_of_formal_logic 形式逻辑系统]
 +
 +
==指南==
 +
在数学、逻辑和计算机科学中，[https://zh.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E8%AF%AD%E8%A8%80 形式语言（Formal language）]是用精确的数学或机器可处理的公式定义的语言。
 +
 +
在计算机科学和数理逻辑中，证明助手或交互式定理检验器是一种软件工具，通过人机协作来协助开发形式证明。
  
 
在计算机科学和软件工程领域，形式化方法是使用适当的数学分析以提高设计的可靠性和强健性，适合于软件和硬件系统的描述、开发和验证。
 
在计算机科学和软件工程领域，形式化方法是使用适当的数学分析以提高设计的可靠性和强健性，适合于软件和硬件系统的描述、开发和验证。
第12行： 第72行：
 
非形式化证明是算法，形式化证明是代码。
 
非形式化证明是算法，形式化证明是代码。
  
−
[[文件:Formal-Verification.png]]
+
[[文件:Formal-Verification.png]] [https://deepspec.org DeepSpec] The Science of Deep Specification
  
 
覆盖的核心概念有：
 
覆盖的核心概念有：
 
* 逻辑学中的基本工具，用于准确地提出并论证关于程序的假设，逻辑学被称之为计算机科学的微积分；
 
* 逻辑学中的基本工具，用于准确地提出并论证关于程序的假设，逻辑学被称之为计算机科学的微积分；
−
* 证明助理用于构造严谨的逻辑论据，分为两类：自动定理证明器和证明助理（如：[[Coq]]、[[Agda]]）；
+
* 证明助理用于构造严谨的逻辑论据，分为两类：自动定理证明器和证明助理（如：[[Coq]]、[[Isabelle]]、[[Agda]]）；
 
* 函数式编程思想，同时作为一种编程方法来简化程序的论证，以及架起程序和逻辑学之间的桥梁。
 
* 函数式编程思想，同时作为一种编程方法来简化程序的论证，以及架起程序和逻辑学之间的桥梁。
  
−
==功能==
+
==语言==
−
 
+
[[文件:purely-functional-programming.png]]
−
==指南==
+
[[文件:FStarLang-logo.png|right|FStarLang]]
 +
*在数学、逻辑和计算机科学中，形式语言（[[Formal language]]）是用精确的数学或机器可处理的公式定义的语言。
 +
*[[F*]] [https://github.com/dafny-lang/dafny Dafny]
 +
*[[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.
 +
*[[ML]] [[isabelle]] [https://cakeml.org/ CakeML] A Verified Implementation of ML
 +
*[[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]
 +
*[[Common Lisp]] [http://www.nuprl.org/ PRL Project] Proofs as Programs
 +
*[https://github.com/leanprover Lean] Prover
 +
*[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]]
 +
[[文件:z3-logo.png|right|Z3]]
 +
[[文件:Isabelle-logo.gif|right|isabelle]]
 +
[[文件:Lean-logo.png|right|Lean]]
 +
[[文件:Acl2-logo.png|right|ACL2]]
 
[[文件:deepspec-logo.png|right]]
 
[[文件:deepspec-logo.png|right]]
 +
[[文件:vellvm-logo.jpg|right|Vellvm]]
 +
[[文件:key-logo.png|right|KeY]]
 +
*[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]
 +
*[https://www.higithub.com/?q=proof-assistant proof assistant @ higithub]
 
*[https://deepspec.org DeepSpec] The Science of Deep Specification
 
*[https://deepspec.org DeepSpec] The Science of Deep Specification
 +
*[http://www.cs.ru.nl/%7Efreek/100/ Formalizing 100 Theorems]
 
*[[Coq]]
 
*[[Coq]]
 
*[[Agda]]
 
*[[Agda]]
 +
*[[Lean]]
 
*[[Idris]]
 
*[[Idris]]
 
*[[ACL2]]
 
*[[ACL2]]
−
*[https://github.com/FStarLang/FStar F*] A Proof-oriented Programming Language
+
*[https://groupoid.space/ Groupoid Infinity Institute is doing formalization of mathematics] Made by [[Erlang]]
−
*[https://github.com/SRI-CSL/PVS Prototype Verification System (PVS)] 使用 [[Common Lisp]] 编写
+
*[[Z3|Z3 Theorem Prover]] [https://theory.stanford.edu/~nikolaj/programmingz3.html Programming Z3]
 +
*[[F*]] A Proof-oriented Programming Language
 +
*[https://cvc4.github.io/ CVC4]
 +
*[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://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]]
第39行： 第124行：
 
*[https://github.com/dafny-lang Dafny] is a verification-aware programming language 使用 [[C Sharp|C#]] 编写，采用 MIT 许可证。
 
*[https://github.com/dafny-lang Dafny] is a verification-aware programming language 使用 [[C Sharp|C#]] 编写，采用 MIT 许可证。
 
*[https://ucsd-progsys.github.io/liquidhaskell-tutorial/ Programming with Refinement Types] An Introduction to [https://github.com/ucsd-progsys/liquidhaskell LiquidHaskell]
 
*[https://ucsd-progsys.github.io/liquidhaskell-tutorial/ Programming with Refinement Types] An Introduction to [https://github.com/ucsd-progsys/liquidhaskell LiquidHaskell]
−
*[https://isabelle.in.tum.de/ Isabelle] is a generic proof assistant
+
*[[isabelle]] is a generic proof assistant [https://www.isa-afp.org/ Isabelle 形式化证明存档（Archive of Formal Proofs）]
 +
*[https://github.com/the-little-prover/j-bob The Little Prover]
 +
*[https://github.com/ProofGeneral/PG Proof General] Organize your proofs!
 +
*[https://redprl.org/ The red* family of proof assistants]
 +
*[https://github.com/LogicalAtomist/principia The Principia Rewrite] 《数学原理》重写工程——该项目致力于将罗素与怀特海的《数学原理》使用 Coq 语言完全重写，补全原书的逻辑漏洞，将其中的证明进行 100% 的机器形式化验证。同时，项目还会将 Coq 的证明进行排版，生成和原书风格一致、可检索、排版精致的文本供人类阅读。@Libre盖子
 +
*[http://why3.lri.fr Why3] 是一个用于演绎程序验证（deductive program verification）的平台
 +
*[https://github.com/EasyCrypt EasyCrypt] Computer-Aided Cryptographic Proofs
 +
*[https://www.frama-c.com/ Frama-C] using Why3
 +
*[http://matita.cs.unibo.it/ Matita] interactive theorem prover
 +
*[http://www.nuprl.org/ PRL Project] Proofs as Programs
 +
*[http://smtlib.cs.uiowa.edu/standard.shtml SMT-LIB standrad] Language, Theories, Logics [http://smtlib.cs.uiowa.edu/solvers.shtml SMT solvers] such as [https://yices.csl.sri.com/ Yices 2], [https://github.com/Z3Prover/z3 Z3]
 +
*[http://www.tptp.org/ The TPTP Problem Library for Automated Theorem Proving]
 +
*[https://leanprover.github.io/ Lean theorem prover] [https://leanprover-community.github.io/ Lean community] Lean and its Mathematical Library
 +
*[https://github.com/kframework/kore The Kore Language] K 框架符号执行引擎，[[Haskell]] 编写。
 +
*[[Cardano]] [https://iohk.io/en/research/library/ formal verification]
 +
*[https://www.cl.cam.ac.uk/~jrh13/hol-light/ HOL Light theorem prover] [[OCaml]] 编写
 +
*[https://www.cis.upenn.edu/~stevez/vellvm/ Vellvm] Verifying the [[LLVM]]
 +
*[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://www.key-project.org/ KeY Project]
 +
*[https://www.tptp.org/ TPTP (Thousands of Problems for Theorem Provers)]
 +
*[https://www.gnu.org/software/c-graph GNU C-Graph] Convolution Theorem Visualization（卷积定理的可视化） [[文件:gnu.tiny.png]]
 +
 
 +
==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
 +
 
 +
==研究组织==
 +
[[文件: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]
 +
*[http://verify.inf.usi.ch/ Formal Verification and Security Lab]
 +
*[https://www.cl.cam.ac.uk/research/pls/ Programming, Logic, and Semantics Group] [https://www.cl.cam.ac.uk/research/hvg/ Automated Reasoning Group]
 +
*[https://fsl.cs.illinois.edu/ Formal Systems Laboratory (FSL)]
 +
*[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://shemesh.larc.nasa.gov/fm/ NASA Langley Formal Methods Research Program]
 +
*[https://formalverification.cs.utah.edu/ FORMAL VERIFICATION AT UTAH]
 +
*[https://www.microsoft.com/en-us/research/group/research-software-engineering-rise/ Research in Software Engineering (RiSE)]
  
 
==文档==
 
==文档==
 
*[https://arxiv.org/pdf/1902.08726.pdf A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts]
 
*[https://arxiv.org/pdf/1902.08726.pdf A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts]
 +
*[https://isabelle.in.tum.de/Isar/ Isar] — [https://isabelle.in.tum.de/coursematerial/PSV2009-1/session78/document.pdf A language for structured proofs]
 +
*[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://hol-theorem-prover.org/hol-course.pdf Interactive Theorem Proving (ITP) Course]
 +
*[https://fm.csl.sri.com/SSFT19/ssft19-kkyi.pdf Static Analysis: an Abstract Interpretation Perspective]
 +
*[https://fm.csl.sri.com/SSFT19/viper-lecture.pdf Modular Program Verification]
 +
*[https://fm.csl.sri.com/SSFT19/speaklogicV9.pdf Speaking Logic]
 +
*[https://fm.csl.sri.com/SSFT14/rosette-lecture.pdf Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond]
 +
*[https://bblanche.gitlabpages.inria.fr/CryptoVerif/tutorial/cryptoverif.pdf CryptoVerif: Mechanizing Game-Based Proofs]
 +
*[https://www.kth.se/social/files/596318bc56be5bfdc343d436/itp-course.pdf Interactive Theorem Proving (ITP) Course]
  
 
==图书==
 
==图书==
 +
*[https://www.nuprl.org/book/ 《Implementing Mathematics with The Nuprl Proof Development System》]
 +
*[https://www.amazon.com/Mathematical-Proofs-Transition-Advanced-Mathematics/dp/0134746759 《Mathematical Proofs: A Transition to Advanced Mathematics》] Gary Chartrand, Albert D. Polimeni, Ping Zhang
 
*[https://softwarefoundations.cis.upenn.edu/ 《Software Foundations》] 软件基础系列是对可靠软件的数学基础的广泛介绍。该系列的主要创新之处在于，每一个细节都是百分之百的形式化和机器检查：每一卷的整个文本，包括练习，实际上是Coq证明助手的 "证明脚本"。
 
*[https://softwarefoundations.cis.upenn.edu/ 《Software Foundations》] 软件基础系列是对可靠软件的数学基础的广泛介绍。该系列的主要创新之处在于，每一个细节都是百分之百的形式化和机器检查：每一卷的整个文本，包括练习，实际上是Coq证明助手的 "证明脚本"。
 
*[https://coq-zh.github.io/SF-zh/ 《软件基础》]系列广泛地介绍了可靠软件的数学基础，这是《Software Foundations》中文版。
 
*[https://coq-zh.github.io/SF-zh/ 《软件基础》]系列广泛地介绍了可靠软件的数学基础，这是《Software Foundations》中文版。
 +
*[https://www.cs.princeton.edu/~appel/papers/plcc.pdf 《Program Logics for Certified Compilers》]
 +
*《芯片验证漫游指南：从系统理论到UVM的验证全视界》刘斌
 +
数字集成系统的验证，是提高设计芯片一次流片成功的关键。随着芯片制造工艺的更加精细，芯片制造费用的不断增加，芯片功能越来越复杂，验证的重要性也日益增加。
 +
* 《方程求解与机器证明 基于MMP的问题求解》 科学出版社 2008 高小山、王定康、裘宗燕、杨宏著
 +
*《数学机械化》 科学出版社 2006 吴文俊 著
 +
*《王者之路 机器证明及其应用》 吴文俊、张景中等
 +
建立几何的代数化，使几何问题的求解转化为方程的求解。把几何问题转化为方程求得的解答，表达成几何的定理，这可视为从方程解答导致定理自动发明的某些原始实例。
  
 
==图集==
 
==图集==
第59行： 第201行：
 
image:isabelle-plugin-manager.png|isabelle插件
 
image:isabelle-plugin-manager.png|isabelle插件
 
image:isabelle-implementation.png|isabelle实现
 
image:isabelle-implementation.png|isabelle实现
 +
image:cognitive-science-heptagram.png|认知科学
 +
image:viper.png|Viper
 +
image:Nuprl5-FDL-diagram.png|Nuprl5 FDL
 +
image:FStar-Architecture.png|F*
 +
image:truth-table.png|真值表
 +
image:syntax-of-propositional-logic.png|命题逻辑的符号
 +
image:ITP-Common-Terms-and-Types.png|常见Terms和Types
 +
image:HOL-family-tree.png|HOL家族
 +
image:HOL4-Emacs.png|HOL4 Emacs
 +
image:Automated-Formal-Verification.png|Automated Formal Verification
 +
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设计形式化验证
 +
image:A-Multipurpose-Formal-RISC-V-Specification.png|RISC-V形式化验证
 
</gallery>
 
</gallery>
  
 
==链接==
 
==链接==
−
*[https://flint.cs.yale.edu/flint/index.html Yale FLINT Group]
+
[[文件:runtime-verification.png|right|Runtime Verification]]
−
*[http://verify.inf.usi.ch/ Formal Verification and Security Lab]
+
[[文件:bluespec-logo.png|right|bluespec]]
 +
*[https://runtimeverification.com/ Runtime Verification Inc] We love formal methods
 +
*[http://wiki.bluespec.com/ Bluespec] Open Source RISC-V Cores and Tools
 +
*[https://formal.land/ Formal Land] 对日常生活中的程序（everyday-life programs）进行形式化验证
 +
*[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.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:proof assistant]]
 
[[category:proof assistant]]
 +
[[category:reasoning]]
 +
[[category:mathematics]]
 +
[[category:computer science]]
 
[[category:coq]]
 
[[category:coq]]
 
[[category:agda]]
 
[[category:agda]]
 +
[[category:ACL2]]
 
[[category:OCaml]]
 
[[category:OCaml]]
 
[[category:haskell]]
 
[[category:haskell]]
 +
[[category:lisp]]

2023年8月3日 (四) 23:57的最后版本

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）。

自动化定理证明（Automated theorem proving，ATP）目前是自动推理（Automated reasoning，AR）体系中发展最好的部分，它的目的是为使用电子计算机程序来进行数学定理的证明。对于不同的公理系统，它能够推论出一个定理在此系统下是正确的，还是不可证明的，或者错误的。

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

[编辑] 机器证明

笛卡尔曾有过一个宏伟的设想：”一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。“他把问题问题想得过于简单了。如果他的设想真能实现，那就不仅是数学的机械化，而且是全部科学的机械化。因为，代数求解是可以机械化的。但笛卡尔没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座划时代的桥梁，实现了初等几何问题代数化。这为后来的几何定理机器证明的代数方法打下了基础。p.21

1977年，吴文俊提出的定理机器证明新方法正式发表。使用这新方法（简称吴法），可以在微机上迅速地证明很不简单的几何定理，如西姆松定理、费尔哈定理、莫勒定理等等；还能发现新的不平凡的的几何定理。1989年，访美学者周咸青基于吴法编制的 Lisp 程序（所谓”证明器“）在计算机上证明了512条定理。这些定理大多是不平凡的，其中还有新定理。证明每条定理所用的机器时间一般才几秒钟。p.27-28

《王者之路 机器证明及其应用》吴文俊等

吴氏方法的基本思想是，先把几何问题化为代数问题，再把代数问题化为代数恒等式的检验问题。代数恒等式的检验是机械的，问题的转化过程也是机械的，整个问题也就机械化了。《数学与哲学》张景中，p.156

[编辑] 新闻

[编辑] 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

覆盖的核心概念有：

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

[编辑] 语言

Purely-functional-programming.png

FStarLang

[编辑] 项目

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

[编辑] STEM

[编辑] 研究组织

Automated Reasoning Group
NASA Langley's Formal Methods

[编辑] 文档

[编辑] 图书

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

  • 《方程求解与机器证明 基于MMP的问题求解》 科学出版社 2008 高小山、王定康、裘宗燕、杨宏著
  • 《数学机械化》 科学出版社 2006 吴文俊 著
  • 《王者之路 机器证明及其应用》 吴文俊、张景中等

建立几何的代数化，使几何问题的求解转化为方程的求解。把几何问题转化为方程求得的解答，表达成几何的定理，这可视为从方程解答导致定理自动发明的某些原始实例。

[编辑] 图集

  • 证明助手

  • 规范

  • 验证

  • VST

  • CompCert

  • 希尔伯特演绎系统

  • isabelle

  • isabelle插件

  • isabelle实现

  • 认知科学

  • Viper

  • Nuprl5 FDL

  • F*

  • 真值表

  • 命题逻辑的符号

  • 常见Terms和Types

  • HOL家族

  • HOL4 Emacs

  • Automated Formal Verification

  • HiFrog

  • KeY架构

  • KeY & JML

  • KeY SED

  • VLSI设计形式化验证

  • RISC-V形式化验证

[编辑] 链接

Runtime Verification
bluespec
来自“http://wiki.huihoo.com/wiki/?title=Formal_verification&oldid=166918”
分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱