ACL2 2006: Seattle, Washington, USA

Panagiotis Manolios, Matthew Wilding (Eds.): 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 BibTeX

Session 1

Lee Pike, Mark Shields, John Matthews:
A verifying core for a cryptographic language compiler. 1-10
Electronic Edition (ACM DL) BibTeX
David S. Hardin, Eric W. Smith, William D. Young:
A robust machine code proof framework for highly secure applications. 11-20
Electronic Edition (ACM DL) BibTeX

Session 2

John R. Cowles, Ruben Gamboa:
Unique factorization in ACL2: Euclidean domains. 21-27
Electronic Edition (ACM DL) BibTeX
David Greve:
Parameterized congruences in ACL2. 28-34
Electronic Edition (ACM DL) BibTeX
Sol Swords, William R. Cook:
Soundness of the simply typed lambda calculus in ACL2. 35-39
Electronic Edition (ACM DL) BibTeX

Session 3

Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds:
An embedding of the ACL2 logic in HOL. 40-46
Electronic Edition (ACM DL) BibTeX
Julien Schmaltz, Dominique Borrione:
Towards a formal theory of on chip communications in the ACL2 logic. 47-56
Electronic Edition (ACM DL) BibTeX
Jared Davis:
Memories: array-like records for ACL2. 57-60
Electronic Edition (ACM DL) BibTeX

Session 4

Tony Hoare:
The ideal of verified software. 61-62
Electronic Edition (ACM DL) BibTeX

Session 5

Erik Reeber, Jun Sawada:
Combining ACL2 and an automated verification tool to verify a multiplier. 63-70
Electronic Edition (ACM DL) BibTeX
Ruben Gamboa, John R. Cowles:
Implementing a cost-aware evaluator for ACL2 expressions. 71-80
Electronic Edition (ACM DL) BibTeX
Robert S. Boyer, Warren A. Hunt Jr.:
Function memoization and unique object representation for ACL2 functions. 81-89
Electronic Edition (ACM DL) BibTeX

Session 6

David L. Rager:
Adding parallelism capabilities to ACL2. 90-94
Electronic Edition (ACM DL) BibTeX
Sandip Ray:
Quantification in tail-recursive function definitions. 95-98
Electronic Edition (ACM DL) BibTeX
Warren A. Hunt Jr., Serita M. Nelesen:
Phylogenetic trees in ACL2. 99-102
Electronic Edition (ACM DL) BibTeX
Matt Kaufmann, J. Strother Moore:
Double rewriting for equivalential reasoning in ACL2. 103-106
Electronic Edition (ACM DL) BibTeX

Session 7

Dale Vaillancourt, Rex L. Page, Matthias Felleisen:
ACL2 in DrScheme. 107-116
Electronic Edition (ACM DL) BibTeX
Jared Davis:
Reasoning about ACL2 file input. 117-126
Electronic Edition (ACM DL) BibTeX
Warren A. Hunt Jr., Erik Reeber:
A SAT-based procedure for verifying finite state machines in ACL2. 127-135
Electronic Edition (ACM DL) BibTeX