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