欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2/Agda, C++/Lisp/Haskell
ACL2
来自开放百科 - 灰狐
（版本间的差异）
小 (→形式化验证) |
小 (→形式化验证) |
||
| 第18行： | 第18行： | ||
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____SOFTWARE-VERIFICATION Software-verification] | *[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____SOFTWARE-VERIFICATION Software-verification] | ||
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____PROOF-AUTOMATION Proof-automation] | *[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____PROOF-AUTOMATION Proof-automation] | ||
| + | *[https://www.kestrel.edu/research/apt/ Automated Program Transformations (APT)] 建立在ACL2定理验证器上，可以高度自动化地转换程序和程序规范，所有由APT生成的证明都由定理验证器检查。 | ||
==功能== | ==功能== | ||
2021年12月23日 (四) 13:47的版本
|
您可以在Wikipedia上了解到此条目的英文信息 ACL2 Thanks, Wikipedia. |
ACL2
目录 |
简介
ACL2 Theorem Prover
ACL2（A Computational Logic for Applicative Common Lisp，应用 Common Lisp 计算逻辑）是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2从设计上支持基于归纳逻辑理论的自动推理，可应用于软件或硬件系统的验证。ACL2的编程语言与实现基于 Common Lisp。ACL2是基于BSD授权发布的开源软件。
ACL2 程序语言可看作是一个函数式（无任何副作用）的 Common Lisp 变体。
编程语言
形式化验证
- Introduction-to-the-theorem-prover
- Hardware-verification
- Software-verification
- Proof-automation
- Automated Program Transformations (APT) 建立在ACL2定理验证器上，可以高度自动化地转换程序和程序规范，所有由APT生成的证明都由定理验证器检查。
功能
指南
Debian
$ sudo apt install acl2 $ acl2 ACL2 !>:doc max
项目
图集
链接
分享您的观点
