ACL2

来自开放百科 - 灰狐
（版本间的差异）
跳转到： 导航, 搜索
小 (→‎文档)
小 (→‎项目)
 
（未显示1个用户的17个中间版本）
第5行： 第5行：
  
 
==简介==
 
==简介==
 +
[[文件:ACL2-logo-small.png|right|ACL2]]
 
ACL2 Theorem Prover
 
ACL2 Theorem Prover
  
第12行： 第13行：
  
 
==功能==
 
==功能==
 +
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=COMMON-LISP____TYPE ALC2 type-related concepts]
  
 
==指南==
 
==指南==
 +
[https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html A Brief ACL2 Tutorial]
 +
 
Debian
 
Debian
 
  $ sudo apt install acl2
 
  $ sudo apt install acl2
第23行： 第27行：
  
 
*[https://www.cs.utexas.edu/users/moore/publications/hyper-card.html Hyper-Card for ACL2 Programming]
 
*[https://www.cs.utexas.edu/users/moore/publications/hyper-card.html Hyper-Card for ACL2 Programming]
 +
 +
函数定义
 +
*defun
 +
*defunc  ;; with contracts
 +
*defunec ;; with contracts extending
  
 
==编程语言==
 
==编程语言==
第39行： 第48行：
 
*[https://z.cash Zcash] 是一种区块链加密货币，通过零知识证明（zero-knowledge proofs）提供保密性。
 
*[https://z.cash Zcash] 是一种区块链加密货币，通过零知识证明（zero-knowledge proofs）提供保密性。
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=BITCOIN____BITCOIN Bitcoin] 库包含[[bitcoin|比特币]]某些方面的形式化模型  
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=BITCOIN____BITCOIN Bitcoin] 库包含[[bitcoin|比特币]]某些方面的形式化模型  
 +
*[https://www.kestrel.edu/research/ethereum/ ACL2 Ethereum Project]
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ETHEREUM____ETHEREUM Ethereum] 库包含[[ethereum|以太坊]]某些方面的形式化模型
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ETHEREUM____ETHEREUM Ethereum] 库包含[[ethereum|以太坊]]某些方面的形式化模型
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____MILAWA Milawa] 是一个类似 ACL2 逻辑的 "自我验证 "定理检验器。
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____MILAWA Milawa] 是一个类似 ACL2 逻辑的 "自我验证 "定理检验器。
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____RP-REWRITER Rp-rewriter] (retain property 保留属性) 是一个经过验证的条款处理器，可以用来替代ACL2的改写器（rewriter）。对于某些情况，在构建公理时可以提供时间效率和便利。
 
*[https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____RP-REWRITER Rp-rewriter] (retain property 保留属性) 是一个经过验证的条款处理器，可以用来替代ACL2的改写器（rewriter）。对于某些情况，在构建公理时可以提供时间效率和便利。
 +
 +
==[[parallel computing|并行计算]]==
 +
[https://www.cs.utexas.edu/users/moore/acl2/v8-5/combined-manual/index.html?topic=ACL2____PARALLEL-PROGRAMMING Parallel programming in ACL2(p)]
  
 
==项目==
 
==项目==
第47行： 第60行：
 
*[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（递增可满足性求解）
 +
*[https://github.com/calebegg/proof-pad Proof Pad] is a web based IDE for ACL2, using a [[Kubernetes]] based backend.
  
 
==文档==
 
==文档==
第53行： 第68行：
 
[https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____XDOC XDOC] is a tool for documenting ACL2 books.
 
[https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____XDOC XDOC] is a tool for documenting ACL2 books.
  
 +
*[https://www.cs.utexas.edu/users/moore/acl2/talks/royal-society/talk.pdf Industrial Hardware and Software Verification with ACL2]
 
*[https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.pdf Industrial Use (of ACL2) for Hardware Verification]
 
*[https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.pdf Industrial Use (of ACL2) for Hardware Verification]
  
第64行： 第80行：
 
*《Design and Verification of Microprocessor Systems for High-Assurance Applications》
 
*《Design and Verification of Microprocessor Systems for High-Assurance Applications》
 
*《Formal Verification of Floating-Point Hardware Design: A Mathematical Approach》
 
*《Formal Verification of Floating-Point Hardware Design: A Mathematical Approach》
 +
 +
==STEM==
 +
*[https://www.cs.utexas.edu/users/hunt/class/2021-fall/cs389r/cs389r.html Recursion and Induction -- CS 389r] [https://www.cs.utexas.edu/users/hunt/class/2021-fall/cs389r/lecture-6.pdf Recursion and Induction]
  
 
==图集==
 
==图集==
 +
<gallery>
 +
image:acl2-system-architecture.gif|ACL2系统架构
 +
image:ACL2-Formal-Verification-Design-Flow.png|ACL2形式化验证设计流程
 +
image:ACL2-Formal-Verification-Flow.png|ACL2形式化验证流程
 +
image:Proof-Pad-on-Windows.png|Proof Pad
 +
</gallery>
  
 
==链接==
 
==链接==
 
*[http://www.cs.utexas.edu/users/moore/acl2/ ACL2官网]
 
*[http://www.cs.utexas.edu/users/moore/acl2/ ACL2官网]
 
*[http://docs.huihoo.com/lisp/acl2 ACL2文档]
 
*[http://docs.huihoo.com/lisp/acl2 ACL2文档]
 +
*[https://www.kestrel.edu/ Kestrel Institute]
 +
*[https://www.cs.utexas.edu/users/hunt/ Warren A. Hunt, Jr.]
 +
*[http://www.computationallogic.com/ Computational Logic Inc.(CLI)]
  
 
[[category:lisp]]
 
[[category:lisp]]
 +
[[category:reasoning]]
 
[[category:proof assistant]]
 
[[category:proof assistant]]
 
[[category:formal]]
 
[[category:formal]]

2022年10月13日 (四) 09:25的最后版本

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

ACL2

Acl2-logo.png

目录

[编辑] 简介

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 变体。

[编辑] 功能

[编辑] 指南

A Brief ACL2 Tutorial

Debian 

$ sudo apt install acl2
$ acl2
GCL (GNU Common Lisp) ...
ACL2>(@ acl2-version)
"ACL2 Version 8.4"
ACL2 !>:doc max

函数定义

  • defun
  • defunc  ;; with contracts
  • defunec ;; with contracts extending

[编辑] 编程语言

  • ACL2 programming language
  • Yul 编程语言被用作编译以 Solidity 语言编写的Ethereum 智能合约的中间语言。然而，Yul 被设计成比 Solidity 更通用，并可能很快找到更多的应用。
  • Imp 是一种简单的编程语言，主要用于教学目的。
  • Java An ACL2 library for Java

[编辑] 形式化验证

[编辑] 并行计算

Parallel programming in ACL2(p)

[编辑] 项目

ACL2S

[编辑] 文档

ACL2 有自己的一套文档、图书 出版系统，文档的源文件都是 .lisp 结尾, xdoc 包，defxdoc constructors（构造器）函数组成。

XDOC is a tool for documenting ACL2 books.

[编辑] 图书

Books and Papers

  • 《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

[编辑] 图集

  • ACL2系统架构

  • ACL2形式化验证设计流程

  • ACL2形式化验证流程

  • Proof Pad

[编辑] 链接

来自“http://wiki.huihoo.com/wiki/?title=ACL2&oldid=166101”
分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱