ACL2 ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses.

Current Version:   2.3 License Type:   GPL

Home Site: http://www.cs.utexas.edu/users/moore/acl2/ Source Code Availability:   Yes Available Binary Packages: Debian Package:   No RedHat RPM Package:   No Other Packages:   Yes (tar.gz) Targeted Platforms: Mac, Sparc, Linux, and other Unix Software/Hardware Requirements: GCL or Allegro Common Lisps

Other Links: None Mailing Lists/USENET News Groups: None User Comments: None See A Screen Shot? (Not Yet)

  SAL Home   |   Programming   |   Languages & Compilers