Program

Tuesday, August 15th

Tuesday's program is also available with abstracts or side by side with other meetings.

08:50‑09:00  Welcome and Opening Remarks
Location: Suite 3102

08:50

Pete Manolios and Matt Wilding

09:00‑10:00  Session 1
Chair: J Strother Moore
Location: Suite 3102

09:00	Lee Pike , Mark Shields and John Mattews A Verifying Core for a Cryptographic Language Compiler
09:30	David Hardin, Eric Smith and William Young A Robust Machine Code Proof Framework for Highly Secure Applications

10:00‑10:30  Break

10:30‑11:45  Session 2
Chair: Jose Luis Ruiz-Reina
Location: Suite 3102

10:30	John Cowles and Ruben Gamboa Unique Factorization in ACL2: Euclidean Domains
11:00	David Greve Generalized Congruences in ACL2
11:30	Sol Swords and William R. Cook Soundness of the Simply Typed Lambda Calculus in ACL2
11:45	"Matt Kaufmann, J Strother Moore An Overview of Recent and Upcoming ACL2 Developments

12:30‑14:00  Lunch break

14:00‑15:15  Session 3
Chair: Matt Wilding
Location: Willow A

14:00	Mike Gordon, Warren A. Hunt, Jr. , Matt Kaufmann and James Reynolds An Embedding of the ACL2 Logic in HOL
14:30	Julien Schmaltz and Dominique Borrione Towards a Formal Theory of On Chip Communications in the ACL2 Logic
15:00	Jared Davis Memories: Array-like Records for ACL2
15:15	Matt Kaufmann, J Strother Moore ACM Software System Award Remarks

15:30‑16:00  Break

16:00‑16:45  Invited Talk
Location: Willow A

16:00

Tony Hoare (Microsoft Research) The Ideal of Verified Software

16:45‑18:15  Session 4: Panel: Grand Challenge Problems for the ACL2 Community
Chair: Pete Manolios
Location: Willow A

16:45

David Hardin, Tony Hoare, Gerard Holzmann, J Strother Moore, ... Panel

19:00‑21:30  Workshop Dinner
Location: outside hotel

Wednesday, August 16th

Wednesday's program is also available with abstracts or side by side with other meetings.

09:00‑10:30  Session 5
Chair: Matt Kaufmann
Location: Metropolitan B

09:00	Erik Reeber and Jun Sawada Combining ACL2 and an Automated Verification Tool to Verify a Multiplier
09:30	Ruben Gamboa and John Cowles Implementing a Cost-Aware Evaluator for ACL2 Expressions
10:00	Robert S. Boyer and Warren A. Hunt, Jr. Function Memoization and Unique Object Representation for ACL2 Functions

10:30‑11:00  Break

11:00‑12:00  Session 6
Chair: Ruben Gamboa
Location: Metropolitan B

11:00	David L. Rager Adding Parallelism Capabilities to ACL2
11:15	Sandip Ray Quantification in Tail-recursive Function Definitions
11:30	Warren A. Hunt, Jr. and Serita M. Nelesen Phylogenetic Trees in ACL2
11:45	Matt Kaufmann and J Strother Moore Double Rewriting for Equivalential Reasoning in ACL2

12:00‑13:30  Rump Session (Part of Session 6)
Location: Metropolitan B

12:00	Bill Bevier and David Russinoff Formally Modeling the x86 Instruction Set Architecture
12:05	Warren Hunt BDDs
12:10	Peter Dillinger, Pete Manolios, J Strother Moore, and Daron Vroon ACL2s: The ACL2 Sedan
12:15	J Strother Moore Semi-Automatic Functional Instantiation
12:20	David Russinoff A Unified Mathematical Theory of Register-Transfer Logic and Computer Arithmetic
12:25	Matt Kaufmann, Pete Manolios, J Strother Moore, and Daron Vroon Adding Calling Context Graphs to ACL2 for Improved Termination Analysis

12:30‑14:00  Lunch break

14:00‑15:30  Session 7
Chair: David Russinoff
Location: Metropolitan B

14:00	Dale Vaillancourt , Rex Page and Matthias Felleisen ACL2 in DrScheme
14:30	Jared Davis Reasoning about ACL2 File Input
15:00	Erik Reeber and Warren A. Hunt, Jr. A SAT-Based Procedure for Verifying Finite State Machines in ACL2

15:30‑16:00  Break

16:00‑17:30  Session 8
Chair: Warren Hunt
Location: Metropolitan B

16:00	Matt Kaufmann, J Strother Moore, All Discussion on Possible Future Enhancements to ACL2
16:45	Pete Manolios, Matt Wilding, All Business Meeting