[FOM] ACL2 2009 Call for Participation

Thu Apr 2 00:18:50 EDT 2009

[ Apologies if you get several copies of this call for participation.
  Please share it with students and colleagues who may be interested
  in the workshop. ]

===============================================================================
                         CALL FOR PARTICIPATION
===============================================================================
                            ACL2 2009
International Workshop on the ACL2 Theorem Prover and Its Applications
                           May 11-12, 2009
                   Northeastern University, Boston, MA, USA
                     http://www.cs.utexas.edu/~sandip/acl2-09/

                        In cooperation with ACM SIGPLAN

           ----------------------------------------------------
                Early Registration Deadline: April 12, 2009
           ----------------------------------------------------

ACL2 2009 is the eighth in a series of workshops on the ACL2 Theorem
Prover and Its Applications.  ACL2 is the most recent incarnation of
the Boyer-Moore family of theorem provers, for which Robert Boyer,
Matt Kaufmann, and J 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
specification and verification of computing systems.  The ACL2
workshops occur at approximately 18-month intervals and provide a
major technical forum for researchers to present and discuss
improvements and extensions to the theorem prover, comparisons of ACL2
with other systems, and applications of ACL2 in formal verification.

Invited Keynote
========================================================================
Clarke Barrett (NYU)
>From SAT to SMT: Successes and Challenges

Panel
=======================================================================
What is the Future of Theorem Proving?

PROGRAM 

Monday May 11

8:30 - 8:50 Registration/Coffee

8:50 - 9:00  Sandip Ray and David Russinoff
             Welcome and Opening Remarks

Session 1

9:00 - 9:25 Rob Sumners
            User Control and Direction of a More Efficient Simplifier in ACL2

9:25 - 9:50  J Moore
             Automatically Computing Functional Instantiations

9:50 - 10:05 Robert Boyer and Warren Hunt
             Symbolic Simulation in ACL2

10:05 - 10:20 Hanbing Liu
              Proving A Specific Type Of Inequality Theorems in ACL2: a bind-free experience report

10:20 - 10:35 (Short Break)

Session 2

10:35 - 10:50 Rex Page
             Computational Logic in the Undergraduate Curriculum

10:50 - 11:15 Carl Eastlund and Matthias Felleisen
              Automatically Verified GUI Programs

11:15 - 11:30 Carl Eastlund
              DoubleCheck Your Theorems

11:30 - 11:55 Antonio Garcia-Dominguez, Francisco Palomo-Lozano and Inmaculada Medina-Bulo
              Hypertext Navigation of ACL2 Proofs with XMLEye

11:55 - 1:25 (Lunch)

Session 3

1:25 - 1:50 Ruben Gamboa and John Cowles
            Inverse Functions in ACL2(r)

1:50 - 2:15 Matt Kaufmann
            Abbreviated Output for Input in ACL2

2:15 - 3:00 Matt Kaufmann and J Moore
            New and Desired Features of ACL2

3:00 - 3:30 (Long Break)

Session 4

3:30 - 3:45 Ryan Ralston
            ACL2-Certified AVL Trees

3:45 - 4:00 Fares Fares and Steve Roach
            Proof of Transitive Closure Property of Directed Acyclic Graphs

4:00 - 4:15 John Cowles and Ruben Gamboa
            \triangle = \square

4:15 - 4:30 (Short Break)

Session 5 (Moderator: Pete Manolios)

4:30 - 6:00 Panel: What is the Future of Theorem Proving?

7:30 - 9:00 Workshop Dinner
           Massimino's Restaurant, 207 Endicott Street

Tuesday May 12

8:30 - 9:00 Coffee

Session 6

9:00 - 9:25 Matt Kaufmann, Jacob Kornerup, Mark Reitblatt
           Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover

9:25 - 9:50 Laurence Pierre, Renauld Clavel, and Regis Leveugle
           ACL2 for the Verification of Fault-Tolerance Properties: First Results

9:50 - 10:15 David Hardin and Samuel Hardin
            Efficient, Formally Verifiable Data Structures using ACL2 Single-Threaded Objects for High-Assurance Systems

10:15 - 10:30 David Rager
              An Executable Model for Security Protocol JFKr

10:30 - 11:00 (Break)

Session 7

11:00 - 11:55 TBA
             Rump Session

11:55 - 1:25 (Lunch)

Session 8

1:25 - 2:15 Clark Barrett, Invited Keynote Talk
           From SAT to SMT: Successes and Challenges

2:15 - 2:30 (Short Break)

Session 9

2:30 - 2:45 David Greve
            Automated Reasoning With Quantified Formulae

2:45 - 3:10 David Greve
            Assuming Termination

3:10 - 3:25 (Short Break)

Session 10

3:25 - 3:40 Tom van der Broek and Julien Schmaltz
           A Generic Implementation Model for the Formal Verification
of Networks-on-Chips

3:40 - 4:05 Freek Verbeek and Julien Schmaltz
           Formal Validation of Deadlock Prevention in Networks-on-Chips

4:05 - 4:20 (Short Break)

Session 11

4:20 - 4:45 TBA
           Rump Session

4:45 - 5:00 (Short Break)

Session 12

5:00 - 5:30 Matt Kaufmann, J Moore, and All
           Discussion on Possible Future Enhancements to ACL2

5:30 - 6:00 Sandip Ray, David Russinoff, and All
           Business Meeting

==============================================================================

ORGANIZATION

Co-Chairmen:         Sandip Ray,  University of Texas at Austin, USA 
                     David Russinoff, 	Advanced Micro Devices, Inc., USA
Local Arrangements:  Panagiotis Manolios, Northeastern University, USA
Publications:        Ruben Gamboa, University of Wyoming 

Steering Committee:  John Cowles, University of Wyoming, USA 
		     Ruben Gamboa, University of Wyoming, USA 
		     Matt Kaufmann, University of Texas at Austin, USA 
		     Panagiotis Manolios, Northeastern University, USA 
		     J Strother Moore, University of Texas at Austin, USA 
		     Jun Sawada, IBM Austin Research Laboratory, USA
		     Matt Wilding, Rockwell Collins, Inc., USA

==============================================================================
PROGRAM COMMITTEE

  * John Cowles, University of Wyoming, USA 
  * Ruben Gamboa, University of Wyoming, USA 
  * Mike Gordon, Cambridge University, UK 
  * Matt Kaufmann, University of Texas at Austin, USA 
  * Francisco Palomo Lozano, Universidad de Cadiz, Spain 
  * Panagiotis Manolios, Northeastern University, USA 
  * John Matthews, Galois, Inc., USA 
  * J Strother Moore, University of Texas at Austin, USA 
  * Rex Page, University of Oklahoma, USA
  * Jun Sawada, IBM Austin Research Laboratory, USA
  * Julien Schmaltz, Radboud University, Nijmegen, the Netherlands
  * Natarajan Shankar, SRI International, USA 
  * Rob Sumners, Advanced Micro Devices, Inc., USA 
  * Freek Wiedijk, Radboud University, Nijmegen, the Netherlands
  * Matt Wilding, Rockwell Collins, Inc., USA