Monday, July 14: Workshop, Day 2
8:30	Breakfast
9:00	Announcements
9:10	J Strother Moore	Memory Taggings and Dynamic Data Structures
9:40	J Strother Moore	Inductive Assertions and Operational Semantics -- Long Version
10:10	Short break
10:25	David Greve, Matthew Wilding	Typed ACL2 Records
10:45	David Greve, Matthew Wilding	Using MBE to Speed a Verified Graph Pathfinder
11:05	Long break (refreshments)
11:35	Hanbing Liu	A Solution to the Rockwell Challenge
12:05	Tao Song, Jim Alves-Foss, Calvin Ko, Cui Zhang, Karl Levitt	Using ACL2 to Verify Security Properties of Specification-based Intrusion Detection Systems
12:25	Lunch
14:25	Julien Schmaltz, Ghiath Al Sammane, Dominique Borrione, Pierre Ostier, Diana Toma	Combining ACL2 and Mathematica for the Symbolic Simulation of Digital Systems
14:45	Julien Schmaltz, Dominique Borrione	Validation of a parameterized bus architecture using ACL2
15:05	Short break
15:20	Ruben Gamboa, Mark Patterson	Polymorphism in ACL2
15:50	Ruben Gamboa	Writing Literate Proofs with XML Tools
16:10	Long break (refreshments)
16:40	Sandip Ray, John Matthews, Mark Tuttle	Certifying Compositional Model Checking Algorithms in ACL2
17:10	Vernon Austel	Implementing abstract types in ACL2
17:30		General Discussion (ACL2 enhancements, time/place of next workshop)
18:00	Workshop ends