Sciweavers

Share
ACL2
2006
ACM
9 years 4 days 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
ACL2
2006
ACM
9 years 4 days ago
Quantification in tail-recursive function definitions
We investigate the logical issues behind axiomatizing equations that contain both recursive calls and quantifiers in ACL2. We identify a class of such equations, named extended ta...
Sandip Ray
ACL2
2006
ACM
9 years 2 months ago
Implementing a cost-aware evaluator for ACL2 expressions
One of ACL2’s most interesting features is that it is executable, so users can run the programs that they verify, and debug them during verification. In fact, the ACL2 implemen...
Ruben Gamboa, John R. Cowles
ACL2
2006
ACM
9 years 2 months ago
Function memoization and unique object representation for ACL2 functions
We have developed an extension of ACL2 that includes the implementation of hash-based association lists and function memoization; this makes some algorithms execute more quickly. ...
Robert S. Boyer, Warren A. Hunt Jr.
ACL2
2006
ACM
9 years 2 months ago
ACL2 in DrScheme
Dale Vaillancourt, Rex L. Page, Matthias Felleisen
ACL2
2006
ACM
9 years 2 months ago
Soundness of the simply typed lambda calculus in ACL2
To make it practical to mechanize proofs in programming language metatheory, several capabilities are required of the theorem proving framework. One must be able to represent and ...
Sol Swords, William R. Cook
ACL2
2006
ACM
9 years 2 months ago
Adding parallelism capabilities to ACL2
We have implemented parallelism primitives that permit an ACL2 programmer to parallelize execution of ACL2 functions. We (1) introduce logical definitions for these primitives, (...
David L. Rager
ACL2
2006
ACM
9 years 2 months ago
A verifying core for a cryptographic language compiler
A verifying compiler is one that emits both object code and a proof of correspondence between object and source code.1 We report the use of ACL2 in building a verifying compiler f...
Lee Pike, Mark Shields, John Matthews
books