A-A+

证明辅助工具 Coq

2016年07月28日 Linux 软件 暂无评论 阅读 93 次

Coq 是一款交互式证明辅助工具,采用OCaml开发。Coq提供一套证明系统,可以编写证明,检查证明。Coq也提供一套形式化语言,可编写数学算法、定义、定理。Coq也可以用于程序的正确性证明(比如操作系统的安全性和编译器的正确性)。

标签:

给我留言

Copyright © SEARU.ORG 保留所有权利.   Theme  Ality 网站地图 360网站安全检测平台

用户登录

分享到: