Email Gateway (Aug 18 2022 at 13:17): Email Gateway (Aug 18 2022 at 13:17):From: Sandip Ray <sandip@cs.utexas.edu>
[ 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
Last updated: May 03 2024 at 12:27 UTC