default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDACL2 2006: Seattle, Washington, USA
- Panagiotis Manolios, Matthew Wilding:
Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006. ACM 2006, ISBN 0-9788493-0-2
Session 1
- Lee Pike, Mark Shields, John Matthews:
A verifying core for a cryptographic language compiler. 1-10 - David S. Hardin, Eric Whitman Smith, William D. Young:
A robust machine code proof framework for highly secure applications. 11-20
Session 2
- John R. Cowles, Ruben Gamboa:
Unique factorization in ACL2: Euclidean domains. 21-27 - David A. Greve:
Parameterized congruences in ACL2. 28-34 - Sol Swords
, William R. Cook:
Soundness of the simply typed lambda calculus in ACL2. 35-39
Session 3
- Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds:
An embedding of the ACL2 logic in HOL. 40-46 - Julien Schmaltz, Dominique Borrione:
Towards a formal theory of on chip communications in the ACL2 logic. 47-56 - Jared Davis:
Memories: array-like records for ACL2. 57-60
Session 4
- Tony Hoare:
The ideal of verified software. 61-62
Session 5
- Erik Reeber, Jun Sawada:
Combining ACL2 and an automated verification tool to verify a multiplier. 63-70 - Ruben Gamboa, John R. Cowles:
Implementing a cost-aware evaluator for ACL2 expressions. 71-80 - Robert S. Boyer, Warren A. Hunt Jr.:
Function memoization and unique object representation for ACL2 functions. 81-89
Session 6
- David L. Rager:
Adding parallelism capabilities to ACL2. 90-94 - Sandip Ray:
Quantification in tail-recursive function definitions. 95-98 - Warren A. Hunt Jr., Serita M. Nelesen:
Phylogenetic trees in ACL2. 99-102 - Matt Kaufmann, J Strother Moore:
Double rewriting for equivalential reasoning in ACL2. 103-106
Session 7
- Dale Vaillancourt, Rex L. Page, Matthias Felleisen:
ACL2 in DrScheme. 107-116 - Jared Davis:
Reasoning about ACL2 file input. 117-126 - Warren A. Hunt Jr., Erik Reeber:
A SAT-based procedure for verifying finite state machines in ACL2. 127-135
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-02-14 22:47 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
