For full workshop information, please visit the workshop's home page, http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/.
| 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 | |