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