Sciweavers

ACL2
2006
ACM
14 years 2 months ago
Combining ACL2 and an automated verification tool to verify a multiplier
We have extended the ACL2 theorem prover to automatically prove properties of VHDL circuits with IBM's Internal SixthSense verification system. We have used this extension to...
Erik Reeber, Jun Sawada
TPHOL
2008
IEEE
14 years 5 months ago
An ACL2 Tutorial
We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start on a path towards effective use of ACL2; to...
Matt Kaufmann, J. Strother Moore