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

Session 1

Lee Pike, Mark Shields, John Matthews:
A verifying core for a cryptographic language compiler. 1-10
David S. Hardin, Eric W. 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 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

Last update Wed Feb 15 04:53:17 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page