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 |