ACL2 2007
International Workshop on the ACL2 Theorem Prover and its Applications
http://www.cs.uwyo.edu/~ruben/acl2-07
ADVANCE PROGRAM
November 15-16, 2007 in Austin, Texas
Hosted by FMCAD 2007
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 |
PROCEEDINGS
Workshop proceedings can be purchased separately at lulu.com.