Formal verification

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(简介)
(图集)
第37行: 第37行:
 
image:deepspec.png|验证
 
image:deepspec.png|验证
 
image:Verified-Software-Toolchain.jpg|VST
 
image:Verified-Software-Toolchain.jpg|VST
 +
image:compcert-diagram.png|CompCert
 
</gallery>
 
</gallery>
  

2021年12月20日 (一) 11:49的版本

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

Proof assistant

目录

简介

Proof assistant 证明助理(证明助手)

这里包含计算机辅助定理证明、Coq 证明助理、函数式编程、操作语义、用于论证软件的逻辑和技术、静态类型系统、基于性质的随机测试、以及对实践中编程代码的验证等。

Formal-Verification.png

覆盖的核心概念有:

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

功能

指南

项目

Deepspec-logo.png

图书

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

图集

链接

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

变换
操作
导航
工具箱