Day 2 Schedule, ACL2-2004

For full workshop information, please visit the workshop's home page,

8:30 Breakfast
9:00 Welcome
  Session 6 (Chair: J Moore)
9:05 Wilfred Legato Generic Theories as Proof Strategies: A Case Study for Weakest Precondition Style Proofs
9:35 Warren A Hunt, Jr.,
Robert Bellarmine Krug (speaker),
J Moore
Integrating Nonlinear Arithmetic into ACL2
10:05 Short break
  Session 7 (Chair: Ruben Gamboa)
10:25 David Greve,
Raymond Richards,
Matthew Wilding (speaker)
A Summary of Intrinsic Partitioning Verification
10:55 David Greve Address Enumeration and Reasoning Over Linear Address Spaces
11:25 Long break
  Session 8 (Chair: Robert Krug)
11:55 Eric Smith (speaker),
Serita Nelesen,
David Greve,
Matthew Wilding,
Raymond Richards
An ACL2 Library for Bags (Multisets)
12:15 Raymond Richards (speaker),
David Greve,
Matthew Wilding,
W. Mark Vanfleet
The Common Criteria, Formal Methods and ACL2
12:35 Lunch
  Session 9 (Chair: Dave Greve)
14:20 Bill Young Reverse Abstraction in ACL2
14:40 Jim Alves-Foss,
Carol Taylor (speaker)
An Analysis of the GWV Security Policy
15:00 Short break
  Session 10 (Chair: Anna Slobodova)
15:15 Julien Schmaltz (speaker),
Dominique Borrione
A Functional Specification and Validation Model for Networks on Chip in the ACL2 Logic
15:45 Diana Toma (speaker),
Dominique Borrione
Verification of a cryptographic circuit: SHA-1 using ACL2
16:05 Long break
  Session 11 (Chair: Jun Sawada)
16:35 John Cowles,
Ruben Gamboa (speaker),
Nadya Kuzmina
Axiomatic Events in ACL2(r): A Story of defun, defun-std, and encapsulate
17:05 John Cowles (speaker),
Ruben Gamboa
Contributions to the Theory of Tail Recursive Functions
17:25 ALL General Discussion (e.g., ACL2 enhancements and time/place of next workshop)
18:00 Workshop ends