- 2011
- Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios
:
Integrating Testing and Interactive Theorem Proving. ACL2 2011: 4-19 - John R. Cowles, Ruben Gamboa:
Verifying Sierpinski and Riesel Numbers in ACL2. ACL2 2011: 20-27 - Mike Dahlin, Ryan Johnson, Robert Bellarmine Krug, Michael McCoyd, William D. Young:
Toward the Verification of a Simple Hypervisor. ACL2 2011: 28-45 - Matt Kaufmann, J Strother Moore:
How Can I Do That with ACL2? Recent Enhancements to ACL2. ACL2 2011: 46-60 - Peter Reid, Ruben Gamboa:
Implementing an Automatic Differentiator in ACL2. ACL2 2011: 61-69 - Peter-Michael Seidel:
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback. ACL2 2011: 70-83 - Sol Swords, Jared Davis:
Bit-Blasting ACL2 Theorems. ACL2 2011: 84-102 - Freek Verbeek, Julien Schmaltz:
Formal verification of a deadlock detection algorithm. ACL2 2011: 103-112 - David S. Hardin, Julien Schmaltz:
Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011. EPTCS 70, 2011 [contents] - 2006
- Robert S. Boyer, Warren A. Hunt Jr.:
Function memoization and unique object representation for ACL2 functions. ACL2 2006: 81-89 - John R. Cowles, Ruben Gamboa:
Unique factorization in ACL2: Euclidean domains. ACL2 2006: 21-27 - Jared Davis:
Memories: array-like records for ACL2. ACL2 2006: 57-60 - Jared Davis:
Reasoning about ACL2 file input. ACL2 2006: 117-126 - Ruben Gamboa, John R. Cowles:
Implementing a cost-aware evaluator for ACL2 expressions. ACL2 2006: 71-80 - Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds:
An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46 - David A. Greve:
Parameterized congruences in ACL2. ACL2 2006: 28-34 - David S. Hardin, Eric Whitman Smith, William D. Young:
A robust machine code proof framework for highly secure applications. ACL2 2006: 11-20 - Tony Hoare:
The ideal of verified software. ACL2 2006: 61-62 - Warren A. Hunt Jr., Serita M. Nelesen:
Phylogenetic trees in ACL2. ACL2 2006: 99-102 - Warren A. Hunt Jr., Erik Reeber:
A SAT-based procedure for verifying finite state machines in ACL2. ACL2 2006: 127-135 - Matt Kaufmann, J Strother Moore:
Double rewriting for equivalential reasoning in ACL2. ACL2 2006: 103-106 - Lee Pike, Mark Shields, John Matthews:
A verifying core for a cryptographic language compiler. ACL2 2006: 1-10 - David L. Rager:
Adding parallelism capabilities to ACL2. ACL2 2006: 90-94 - Sandip Ray:
Quantification in tail-recursive function definitions. ACL2 2006: 95-98 - Erik Reeber, Jun Sawada:
Combining ACL2 and an automated verification tool to verify a multiplier. ACL2 2006: 63-70 - Julien Schmaltz, Dominique Borrione:
Towards a formal theory of on chip communications in the ACL2 logic. ACL2 2006: 47-56 - Sol Swords, William R. Cook:
Soundness of the simply typed lambda calculus in ACL2. ACL2 2006: 35-39 - Dale Vaillancourt, Rex L. Page, Matthias Felleisen:
ACL2 in DrScheme. ACL2 2006: 107-116 - 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 [contents]
