Accepted Papers

Dale Vaillancourt, Rex Page, and Matthias Felleisen
ACL2 in DrScheme

David Hardin, Eric Smith, and William Young
A Robust Machine Code Proof Framework for Highly Secure Applications

Sandip Ray
Quantification in Tail-recursive Function Definitions

Jared Davis
Memories: Array-like Records for ACL2

Mike Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds
An Embedding of the ACL2 Logic in HOL

Lee Pike, Mark Shields, and John Mattews
A Verifying Core for a Cryptographic Language Compiler

Warren A. Hunt, Jr., Serita M. Nelesen
Phylogenetic Trees in ACL2

Erik Reeber, Warren A. Hunt, Jr.
A SAT-Based Procedure for Verifying Finite State Machines in ACL2

Julien Schmaltz, Dominique Borrione
Towards a Formal Theory of On Chip Communications in the ACL2 Logic

David L. Rager
Adding Parallelism Capabilities to ACL2

Erik Reeber, Jun Sawada
Combining ACL2 and an Automated Verification Tool to Verify a Multiplier

Jared Davis
Reasoning about ACL2 File Input

John Cowles, Ruben Gamboa
Unique Factorization in ACL2: Euclidean Domains

Sol Swords, William R. Cook
Soundness of the Simply Typed Lambda Calculus in ACL2

David Greve
Generalized Congruences in ACL2

Matt Kaufmann, J Strother Moore
Double Rewriting for Equivalential Reasoning in ACL2

Robert S. Boyer, Warren A. Hunt, Jr.
Function Memoization and Unique Object Representation for ACL2 Functions

Ruben Gamboa, John Cowles
Implementing a Cost-Aware Evaluator for ACL2 Expressions