Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CORR
2004
Springer
107views Education» more  CORR 2004»
11 years 1 months ago
Encapsulation for Practical Simplification Procedures
ACL2 was used to prove properties of two simplification procedures. The procedures differ in complexity but solve the same programming problem that arises in the context of a reso...
Olga Shumsky Matlin, William McCune
JAR
2007
83views more  JAR 2007»
11 years 1 months ago
Theory Extension in ACL2(r)
ACL2(r) is a modified version of the theorem prover ACL2 that adds support for the irrational numbers using non-standard analysis. It has been used to prove basic theorems of anal...
Ruben Gamboa, John R. Cowles
JAR
2006
103views more  JAR 2006»
11 years 1 months ago
A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures
We describe an approach to verifying bit-level pipelined machine models using a combination of deductive reasoning and decision procedures. While theorem proving systems such as AC...
Panagiotis Manolios, Sudarshan K. Srinivasan
FMCAD
2006
Springer
11 years 5 months ago
An Integration of HOL and ACL2
We describe a link between the ACL2 and HOL mechanical proof assistants that enables the strengths of each system to be deployed smoothly within a single formal development. Severa...
Michael J. C. Gordon, James Reynolds, Warren A. Hu...
CAV
1998
Springer
175views Hardware» more  CAV 1998»
11 years 5 months ago
An ACL2 Proof of Write Invalidate Cache Coherence
As a pedagogical exercise in ACL2, we formalize and prove the correctness of a write invalidate cache scheme. In our formalization, an arbitrary number of processors, each with its...
J. Strother Moore
CHARME
2003
Springer
103views Hardware» more  CHARME 2003»
11 years 6 months ago
Linear and Nonlinear Arithmetic in ACL2
Abstract. As of version 2.7, the ACL2 theorem prover has been extended to automatically verify sets of polynomial inequalities that include nonlinear relationships. In this paper w...
Warren A. Hunt Jr., Robert Bellarmine Krug, J. Str...
ACL2
2006
ACM
11 years 7 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
11 years 7 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
11 years 7 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
ACL2
2006
ACM
11 years 7 months ago
Double rewriting for equivalential reasoning in ACL2
Several users have had problems using equivalence-based rewriting in ACL2 because the ACL2 rewriter caches its results. We describe this problem in some detail, together with a pa...
Matt Kaufmann, J. Strother Moore
books