ACL2 2007
International Workshop on the ACL2 Theorem Prover and its Applications
http://www.cs.uwyo.edu/~ruben/acl2-07
CALL FOR PARTICIPATION
November 15-16, 2007 in Austin, Texas
Hosted by FMCAD 2007
IMPORTANT DATES
| (Early) Registration Deadline: | October 19, 2007 |
|---|---|
| Hotel Deadline: | October 19, 2007 |
WORKSHOP
ACL2 2007 is the major technical forum for users of the ACL2 theorem proving system and is the seventh in a series of workshops that occur approximately every 18 months. ACL2 is an industrial-strength automated reasoning system that is part of the Boyer-Moore family of theorem provers, for which its authors received the 2005 ACM Software System Award. ACL2 2007 is hosted by FMCAD.
INVITED TALKS
Natarajan Shankar, SRI International, Mechanized Metamathematics Revisited
Jeff Kodosky, National Instruments, A Vision for Verification in LabVIEW
PROCEEDINGS
Workshop proceedings can be purchased separately at lulu.com.
PROGRAM
|
Wednesday, November 14 | |
|
|
Banquet |
|
Thursday, November 15 | |
|
Welcome | |
|
|
Welcome |
|
Session 1, Chair: John Cowles | |
|
| |
|
Peter Dillinger, Matt Kaufmann, Pete Manolios | |
|
|
Pythia: Automatic Generation of Counterexamples for ACL2 using Alloy |
|
Alexander Spiridonov, Sarfraz Khurshid | |
|
| |
|
John Erickson | |
|
Session 2, Chair: John Matthews | |
|
| |
|
John Cowles, David Greve, William Young | |
|
| |
|
Gabriel Infante-Lopez | |
|
Invited Talk, Chair: Jun Sawada | |
|
|
Mechanized Metamathematics Revisited |
|
Natarajan Shankar | |
|
Session 3, Chair: Warren Hunt | |
|
| |
|
Mirian Andres, Laureano Lamban, Julio Rubio, Jose Luis Ruiz-Reina | |
|
|
Formal Specification and Validation of Minimal Routing Algorithms for the 2D Mesh |
|
Julien Schmaltz | |
|
Session 4, Chair: Ruben Gamboa | |
|
| |
|
Warren Hunt, Robert S. Boyer | |
|
| |
|
Mike Gordon | |
|
Rump Session 1, Chair: Rex Page | |
|
|
Foundations of Automated Induction for a Structured Mechanized Logic |
|
Matt Kaufmann, J Moore, Sandip Ray | |
|
|
Termination Analysis with Calling Context Graphs |
|
Pete Manolios, Daron Vroon | |
|
|
Combining Deductive Reasoning and Decision Procedures for System-Level Verification |
|
Sudarshan Srinivasan, Pete Manolios | |
|
|
Verifying NoC communication architectures with ACL2 |
|
Julien Schmaltz, Laurence Pierre, Amr Helmy | |
|
|
Automating Formal Verification of Block Ciphers |
|
Eric Smith | |
|
Friday, November 16 | |
|
Welcome | |
|
|
Welcome |
|
Session 5, Chair: Matt Kaufmann | |
|
| |
|
Carl Eastlund, Dale Vaillancourt, Matthias Felleisen | |
|
| |
|
Frank Rimlinger | |
|
| |
|
David Greve | |
|
Update | |
|
|
What's New in ACL2? |
|
Matt Kaufmann | |
|
Invited Talk, Chair: J Strother Moore | |
|
|
A Vision for Verification in LabVIEW |
|
Jeff Kodosky | |
|
Rump Session 2, Chair: Pete Manolios | |
|
|
A Generalized Solution for the While Challenge |
|
Sandip Ray | |
|
|
Pushing the While Language Challenge to Greater Depths |
|
John Cowles | |
|
|
Red-Black Trees for DrACuLa |
|
Ruben Gamboa | |
|
|
Formal Verification of LabVIEW Programs with ACL2 |
|
Matt Kaufmann, Jacob Kornerup, Grant Passmore | |
|
|
Proof reusing: the case of the Hindley algorithm |
|
Diego Sotes, Laureano Lamban, Julio Rubio | |
|
Rump Session 3, Chair: Dave Greve | |
|
|
Specifying the X86 ISA |
|
Warren Hunt | |
|
|
The Milawa rewriter and an ACL2 proof of its soundness |
|
Jared Davis | |
|
|
Using ACL2's Verified Clause Processor Mechanism to Sort Commutative and Associative Operations |
|
Erik Reeber | |
|
|
ACL2s, the ACL2 Sedan |
|
Peter Dillinger, Pete Manolios, Daron Vroon, J Moore | |
|
Discussion | |
|
|
Work Session |
|
Matt Kaufmann | |
ORGANIZATION
|
Organizing Committee | |
|
Chairs: |
Ruben Gamboa, University of Wyoming |
|
Jun Sawada, IBM Austin Research Laboratory | |
|
John Cowles, University of Wyoming | |
PROGRAM COMMITTEE