欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
ACL2
来自开放百科 - 灰狐
(版本间的差异)
小 (→指南) |
小 (→项目) |
||
第54行: | 第54行: | ||
*[https://github.com/acl2/acl2/ ACL2 @ GitHub] | *[https://github.com/acl2/acl2/ ACL2 @ GitHub] | ||
*[http://acl2s.ccs.neu.edu ACL2 Sedan theorem prover (ACL2s)] with [[Eclipse]] IDE | *[http://acl2s.ccs.neu.edu ACL2 Sedan theorem prover (ACL2s)] with [[Eclipse]] IDE | ||
+ | *[https://github.com/biotomas/ipasir ipasir] The [https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=IPASIR____IPASIR Standard Interface] for Incremental Satisfiability Solving(递增可满足性求解) | ||
==文档== | ==文档== |
2022年10月13日 (四) 07:15的版本
您可以在Wikipedia上了解到此条目的英文信息 ACL2 Thanks, Wikipedia. |
ACL2
目录 |
简介
ACL2 Theorem Prover
ACL2(A Computational Logic for Applicative Common Lisp,用于通用Lisp的计算逻辑)是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2 从设计上支持基于归纳逻辑理论的自动推理,可应用于软件或硬件系统的验证。ACL2 使用 Common Lisp。ACL2 采用 BSD三条款许可证,3-clause BSD 与 GNU GPL 兼容。
ACL2 程序语言可看作是一个函数式(无任何副作用)的 Common Lisp 变体。
功能
指南
Debian
$ sudo apt install acl2 $ acl2 GCL (GNU Common Lisp) ... ACL2>(@ acl2-version) "ACL2 Version 8.4" ACL2 !>:doc max
编程语言
- ACL2 programming language
- Yul 编程语言被用作编译以 Solidity 语言编写的Ethereum 智能合约的中间语言。然而,Yul 被设计成比 Solidity 更通用,并可能很快找到更多的应用。
- Imp 是一种简单的编程语言,主要用于教学目的。
- Java An ACL2 library for Java
形式化验证
- Introduction-to-the-theorem-prover
- Hardware-verification
- Software-verification
- Proof-automation
- Automated Program Transformations (APT) 建立在ACL2定理验证器上,可以高度自动化地转换程序和程序规范,所有由APT生成的证明都由定理验证器检查。
- SOFT(二阶函数和定理)是一个模仿ACL2一阶逻辑中的二阶函数和定理的工具。
- Zcash 是一种区块链加密货币,通过零知识证明(zero-knowledge proofs)提供保密性。
- Bitcoin 库包含比特币某些方面的形式化模型
- ACL2 Ethereum Project
- Ethereum 库包含以太坊某些方面的形式化模型
- Milawa 是一个类似 ACL2 逻辑的 "自我验证 "定理检验器。
- Rp-rewriter (retain property 保留属性) 是一个经过验证的条款处理器,可以用来替代ACL2的改写器(rewriter)。对于某些情况,在构建公理时可以提供时间效率和便利。
并行计算
Parallel programming in ACL2(p)
项目
- ACL2 @ GitHub
- ACL2 Sedan theorem prover (ACL2s) with Eclipse IDE
- ipasir The Standard Interface for Incremental Satisfiability Solving(递增可满足性求解)
文档
ACL2 有自己的一套文档、图书 出版系统,文档的源文件都是 .lisp 结尾, xdoc 包,defxdoc constructors(构造器)函数组成。
XDOC is a tool for documenting ACL2 books.
- Industrial Hardware and Software Verification with ACL2
- Industrial Use (of ACL2) for Hardware Verification
图书
- 《A Computational Logic》
- 《Computer-Aided Reasoning: An Approach》
- 《Computer-Aided Reasoning: ACL2 Case Studies》
- 《Essential Logic for Computer Science》
- 《Scalable Techniques for Formal Verification》
- 《Design and Verification of Microprocessor Systems for High-Assurance Applications》
- 《Formal Verification of Floating-Point Hardware Design: A Mathematical Approach》
STEM
图集
链接
分享您的观点