Notes:
| Wednesday, May 25: Day 0 | ||
| 19:30 - 21:30 |
RECEPTION | Loro 2115 South Lamar Blvd. Austin, Texas 78704 (map) |
| Thursday, May 26: Day 1 | ||
| 08:30 | COFFEE and SNACKS | |
| Session 1 (chair: Rob Sumners) | ||
| 09:00 | Welcome | |
| 09:10 | Jade Alglave* (Arm, Inc. and University College London) |
Invited talk 1 Armed cats: formal concurrency modelling at Arm |
| 10:10 | Warren Hunt Vivek Ramanathan* J Moore |
VWSIM: A Circuit Simulator |
| 10:40 | BREAK | |
| Session 2 (chair: Shilpi Goel) | ||
| 11:00 | Alessandro Coglio* | A Complex Java Code Generator
for ACL2 Based on a Shallow Embedding of ACL2 in Java [Note: The link above is to a pdf; here is a link to the animated (.ppsx) version] |
| 11:30 | Alessandro Coglio* | A Proof-Generating C Code
Generator for ACL2 Based on a Shallow Embedding of C in ACL2 [Note: The link above is to a pdf; here is a link to the animated (.ppsx) version] |
| 12:00 | David Hardin* | Hardware/Software Co-Assurance using the Rust Programming Language and ACL2 |
| 12:30 | LUNCH | |
| Session 3 (chair: William Young) | ||
| 14:00 | Ruben Gamboa* Woodrow Gamboa |
All Prime Numbers Have Primitive Roots |
| 14:30 | David Russinoff* | A Formalization of Finite Group Theory |
| 15:00 | Matt Kaufmann* J Moore |
Extended Abstract: Iteration in ACL2, WITH .. DO |
| 15:20 | BREAK | |
| Session 4 (chair: Eric Smith) | ||
| 15:40 | Jagadish Bapanapally* Ruben Gamboa |
A Free Group of Rotations of Rank 2 |
| 16:10 | Rump Session 1 |
|
| 16:40 | BREAK | |
| Session 5 | ||
| 17:00 | Social Hour and Business Meeting | |
| 18:00 | Day 1 program ends | |
| 19:00 - 21:30 |
CONFERENCE DINNER | Fresa's 1703 S 1st St, Austin, TX 78704 (map) |
| Friday, May 27: Day 2 | ||
| 08:30 | COFFEE and SNACKS | |
| Session 1 (chair: Cuong Chau) | ||
| 09:00 | Marijn Heule* (Carnegie Mellon University) |
Invited talk 2 Effective Encodings for Computer-Aided Mathematics |
| 10:00 | Mertcan Temel* | Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2 |
| 10:30 | BREAK | |
| Session 2 (chair: Warren Hunt) | ||
| 11:00 | Alessandro Coglio Eric McCarthy* Stephen Westfold* Daniel Balasubramanian Abhishek Dubey Gabor Karsai |
Syntheto: A Surface Language
for APT and ACL2 [Note: The link above is to a pdf; here is a link to the source .pptx version] |
| 11:30 | Andrew Walter* Panagiotis Manolios |
ACL2s Systems Programming |
| 12:00 | Ruben Gamboa Alicia Thoney* |
Using ACL2 To Teach Students About Software Testing |
| 12:30 | LUNCH | |
| Session 3 (chair: Alessandro Coglio) | ||
| 14:00 | William Young* | Modeling Asymptotic Complexity Using ACL2 |
| 14:30 | David Greve* Jennifer Davis Laura Humphrey |
A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A |
| 15:00 | Matt Kaufmann Rob Sumners* Sol Swords |
Extended Abstract: Stobj-tables |
| 15:20 | BREAK | |
| Session 4 (chair: David Greve) | ||
| 15:40 | Matt Kaufmann* J Moore |
What's New in the ACL2 System |
| 16:10 | Alessandro Coglio* | What's New in the Community Books |
| 16:40 | BREAK | |
| Session 5 (chair: Mertcan Temel) | ||
| 17:00 | David Russinoff* | Properties of the Hebrew Calendar |
| 17:30 | Rump Session 2 |
|
| 18:00 | Workshop ends | |