Published: 20th October 2011
DOI: 10.4204/EPTCS.70
ISSN: 2075-2180

EPTCS 70

Proceedings 10th International Workshop
on the ACL2 Theorem Prover and its Applications
Austin, Texas, USA, November 3-4, 2011

Edited by: David Hardin and Julien Schmaltz

Preface
1
Integrating Testing and Interactive Theorem Proving
Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann and Panagiotis Manolios
4
Verifying Sierpiński and Riesel Numbers in ACL2
John R. Cowles and Ruben Gamboa
20
Toward the Verification of a Simple Hypervisor
Mike Dahlin, Ryan Johnson, Robert Bellarmine Krug, Michael McCoyd and William Young
28
How Can I Do That with ACL2? Recent Enhancements to ACL2
Matt Kaufmann and J Strother Moore
46
Implementing an Automatic Differentiator in ACL2
Peter Reid and Ruben Gamboa
61
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback
Peter-Michael Seidel
70
Bit-Blasting ACL2 Theorems
Sol Swords and Jared Davis
84
Formal verification of a deadlock detection algorithm
Freek Verbeek and Julien Schmaltz
103

Preface

This volume contains the proceedings of ACL2 2011, the Tenth International Workshop on the ACL2 Theorem Prover and its Applications. The workshop was held in Austin, Texas, USA, on November 3-4 2011, and was co-located with the Eleventh Conference on Formal Methods in Computer Aided Design (FMCAD'11). The ACL2 Workshop series provides a major technical forum for researchers to present and discuss improvements and extensions to the ACL2 theorem prover, comparisons of ACL2 with other systems, and applications of ACL2 in formal verification or formalized mathematics.

Workshops have been held at approximately 18 month intervals since 1999. Previous workshops were held in Austin, Grenoble, Boulder, Seattle, and Boston. In 2010, the ninth ACL2 Workshop was combined with the TPHOLs conference series under the name of Interactive Theorem Proving (ITP). ITP 2010 was part of FLoC 2010 and was held in Edinburgh, Scotland, on July 11-14 2010.

ACL2 is the most recent incarnation of the Boyer-Moore family of theorem provers, for which Robert Boyer, Matt Kaufmann and J Strother Moore received the 2005 ACM Software System Award. It is a state-of-the-art automated reasoning system that has been successfully used in academia, government and industry for the specification and verification of computing systems.

The proceedings of ACL2 2011 include eight peer-reviewed papers. Each paper was reviewed by at least three members of the Program Committee. In addition to technical papers, the workshop included two invited talks, "Developer-friendly Contract-based Checking of Functional and Information Flow Properties for Embedded Security Devices" by John Hatcliff (Kansas State University) and "The Guardol Programming Language and Verification System: Syntax, Semantics, and Proof Automation" by Konrad Slind (Rockwell Collins), as well as a panel discussion on "The Future of Software Verification". The panelists were David Greve (Rockwell Collins), John Hatcliff (Kansas State University), Panagiotis Manolios (Northeastern University), J Strother Moore (University of Texas at Austin), and Konrad Slind (Rockwell Collins). The workshop also featured Rump Sessions discussing ongoing research.

We thank the members of the Program Committee and the additional reviewers for providing detailed reviews of all the papers. We also thank the members of the Organizing Committee and the ACL2 Steering Committee for their help and guidance. Special thanks are due to Jo Moore, our local arrangements chair. We also thank Rockwell Collins and the University of Texas at Austin for their sponsorship.

David S. Hardin and Julien Schmaltz
September 2011