ACL2 is a {theorem prover} based on Common Lisp commonly used for the verification of hardware.

[The wiki] is an excellent source of information on the language.

[This work] discusses the verification of AIG graph representations of boolean functions.

[This page] has good programming exercises for ACL2.

Often used in {Emacs} with [Proof General].

[Introduction to ACL2 programming.]

[Computer Aided Reasoning], the textbook out of UT, is likely worth spending time reading as well.

[Pete's site for Computer-Aided Reasoning]: lots of good resources for ACL2/S and working with the technology. Add his setup - or some modification of it - to your emacs configuration as a module!

2021-09-22 52a677b
2021-09-21 7732812
2021-08-19 87d9551
2021-04-24 d005e33
2021-04-24 71b86f7
2021-04-24 3bf560f
2021-01-20 35e386e
2021-01-18 af0b1e0
2020-11-15 a0eccac