ACL2 3.5

ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of models.
ACL2 is a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 stands for "A Computational Logic for Applicative Common Lisp".

It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.

last updated on:
May 26th, 2009, 8:56 GMT
price:
FREE!
homepage:
www.cs.utexas.edu
license type:
GPL (GNU General Public License) 
developed by:
Matt Kaufmann and J S. Moore
category:
ROOT \ Programming \ Code Generators
ACL2
Download Button

In a hurry? Add it to your Download Basket!

user rating

UNRATED
0.0/5
 

0/5

Rate it!

Add your review!

SUBMIT