Formal verification

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(语言)
(语言)
第72行: 第72行:
 
*[[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]
+
*[http://smtlib.cs.uiowa.edu/language.shtml SMT-LIB Language] 包含三大组件:theory declarations, logic declarations, and scripts
  
 
==项目==
 
==项目==

2022年2月18日 (五) 06:47的版本

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

Formal verification

目录

简介

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

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

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

Open Provable Foundation

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

这里指包含 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);
  • 函数式编程思想,同时作为一种编程方法来简化程序的论证,以及架起程序和逻辑学之间的桥梁。

语言

项目

Coq
isabelle
Lean
ACL2
Deepspec-logo.png
Vellvm

STEM

研究组织

Automated Reasoning Group

文档

图书

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

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

图集

链接

Runtime Verification
bluespec
  • Runtime Verification Inc We love formal methods
  • Bluespec Open Source RISC-V Cores and Tools
  • Formal Land 对日常生活中的程序(everyday-life programs)进行形式化验证
  • BedRock Systems Unbreakable Foundation for Formally Secured Computing, NOVA is the foundation for the BedRock HyperVisor(BHV), which combines a formally verified secure trusted computing base with VM introspection and policy enforcement.
  • SiFive rapid development of custom hardware solutions, based on RISC-V, Securing The RISC‑V Revolution.
分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱