| Sunday, July 13: Workshop, Day 1 | ||
| 8:30 | Breakfast | |
| 9:00 | Welcome | |
| 9:10 | Matt Kaufmann | A Tool for Simplifying Files of ACL2 Definitions |
| 9:40 | Joe Hendrix | Matrices in ACL2 |
| 10:00 | Panagiotis Manolios Daron Vroon |
Ordinal Arithmetic in ACL2 |
| 10:30 | Long break (refreshments) | |
| 11:10 | Matyas Sustik | Proof of Dickson's Lemma Using the ACL2 Theorem Prover via an Explicit Ordinal Mapping |
| 11:40 | John Cowles, Ruben Gamboa, Jeff Van Baalen |
Using ACL2 Arrrays to Formalize Matrix Algebra |
| 12:00 | Ruben Gamboa, John Cowles, Jeff Van Baalen |
On the Verification of Synthesized Kalman Filters |
| 12:30 | Lunch | |
| 14:30 | Olga Shumsky Matlin, William McCune |
Encapsulation for Practical Simplification Procedures |
| 14:50 | Rob Sumners | Fair Environment Assumptions in ACL2 |
| 15:10 | Diana Toma, Dominique Borrione |
SHA Formalization |
| 15:30 | Long break (refreshments) | |
| 16:10 | David Greve, Matthew Wilding, W. Mark Vanfleet |
A Separation Kernel Formal Security Policy |
| 16:40 | Matt Kaufmann, J Moore |
What's new in ACL2; General Discussion (e.g., ACL2 enhancement requests) |
| 18:00 | End of first day | |