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

PROGRAM

Wednesday, November 14

6:00-9:00	Banquet

Thursday, November 15

Session 1

9:00-9:30	Hacking and Extending ACL2
		Peter Dillinger, Matt Kaufmann, Pete Manolios

9:30-10:00	Pythia: Automatic Generation of Counterexamples for ACL2
		using Alloy
		Alexander Spiridonov, Sarfraz Khurshid

10:00-10:20	Backtracking and Induction in ACL2
		John Erickson

Session 2

10:40-11:00	The While-language Challenge: First Progress
		John Cowles, David Greve, William Young

11:00-11:20	Building Lemmas Using Examples
		Gabriel Infante-Lopez

Invited Talk

1:00-2:00	Mechanized Metamathematics Revisited
		Natarajan Shankar

Session 3

2:20-2:40	Formalizing Simplicial Topology in ACL2
		Mirian Andres, Laureano Lamban, Julio Rubio, 
		Jose Luis Ruiz-Reina

2:40-3:10	Formal Specification and Validation of Minimal Routing
		Algorithms for the 2D Mesh
		Julien Schmaltz

Session 4	

3:30-4:00	Circuit Specification, Abstraction, and Reverse Engineering
		Warren Hunt, Robert S. Boyer

4:00-4:20	Defining a LISP Interpreter in a Logic of Total Functions
		Mike Gordon

Rump Session 1

4:40-5:00	Foundations of Automated Induction for a Structured
		Mechanized Logic
		Matt Kaufmann, J Moore, Sandip Ray

5:00-5:20	Termination Analysis with Calling Context Graphs
		Pete Manolios, Daron Vroon

5:20-5:40	Combining Deductive Reasoning and Decision Procedures for
		System-Level Verification
		Sudarshan Srinivasan, Pete Manolios

5:40-6:00	Automating Formal Verification of Block Ciphers
		Eric Smith
		
Friday, November 16

Session 5

9:00-9:30	ACL2 for Freshmen: First Experiences
		Carl Eastlund, Dale Vaillancourt, Matthias Felleisen

9:30-10:00	Evolution from Debugging to Verification
		Frank Rimlinger

10:00-10:30	Scalable Normalization for Heap Manipulating Functions
		David Greve

Discussion

10:50-11:20	What's New in ACL2?
		Matt Kaufmann

Invited Talk

1:00-2:00	A Vision for Verification in LabVIEW
		Jeff Kodosky

Rump Session 2

2:20-2:30	A Generalized Solution for the While Challenge
		Sandip Ray

2:30-2:40	Pushing the While Language Challenge to Greater Depths
		John Cowles

2:40-2:50	Red-Black Trees for DrACuLa
		Ruben Gamboa

2:50-3:05	Formal Verification of LabVIEW Programs with ACL2
		Matt Kaufmann, Jacob Kornerup, Grant Passmore

3:05-3:20	Proof reusing: the case of the Hindley algorithm
		Diego Sotes, Laureano Lamban, Julio Rubio, Jose Luis Ruiz-Reina

Rump Session 3

3:40-3:55	The Milawa rewriter and an ACL2 proof of its soundness
		Jared Davis

3:55-4:05	Using ACL2's Verified Clause Processor Mechanism to Sort 
		Commutative and Associative Operations
		Erik Reeber

4:05-4:20	Verifying NoC communication architectures with ACL2
		Julien Schmaltz, Laurence Pierre, Amr Helmy

4:20-4:35	Specifying the X86 ISA
		Warren Hunt

4:35-4:50	ACL2s, the ACL2 Sedan
		Peter Dillinger, Pete Manolios, Daron Vroon, J Moore

Discussion

5:10-6:00	Work Session
		Matt Kaufmann

ORGANIZATION

    Chairs

        * Ruben Gamboa, University of Wyoming
        * Jun Sawada, IBM
        * John Cowles, University of Wyoming

    Program Committee

        * David Greve, Rockwell Collins, Inc.
        * John Harrison, Intel Corporation
        * Warren Hunt, University of Texas
        * Deepak Kapur, University of New Mexico
        * Matt Kaufmann, University of Texas
        * Bill Legato, NSA
        * Mike Lowry, NASA
        * Panagiotis Manolios, Northeastern University
        * John Matthews, Galois Connections
        * Jose Meseguer, University of Illinois
        * Paul Miner, NASA
        * J Strother Moore, University of Texas
        * Rex Page, University of Oklahoma
        * Jose Luis Ruiz-Reina, University of Seville
        * Laurence Pierre, Université de Nice Sophia-Antipolis, Laboratoire TIMA
        * David Russinoff, Advanced Micro Devices, Inc.
        * Konrad Slind, University of Utah
        * Matt Wilding, Rockwell Collins, Inc.