Published: 20th October 2011 DOI: 10.4204/EPTCS.70 ISSN: 2075-2180 |
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 |
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