The Taj, 2630 Baseline Rd. (at
Broadway) -- show up between 7:00 and 7:30 pm.
ACL2 is a state-of-the-art automated reasoning system. It grew out of the
Boyer-Moore theorem prover and has been used successfully on a number of
industrial and academic projects. ACL2 is described at http://www.cs.utexas.edu/users/moore/acl2.
The ACL2 workshops provide a forum for presentation and discussion of projects using ACL2 as well as evolution of the tool. Information about the preceding workshops, including slides, papers, and supporting materials, is available on-line:
In case you want a double room, note that spouses not attending the workshop are best listed under Guest. Attendees who want to room together should each fill out the form and indicate their choice to share a room with each other in the "Roommate name" field. There are twin beds in all the rooms and the rooms are non-smoking and also not air conditioned. According to weather.com, the average temperatures in Boulder in July (Fahrenheit) are 87 high, 56 low.
Dorm reservation forms in various formats:
CAV has reserved a block of rooms at the Millenium Hotel through July
12, which apparently is 100 yards from campus. The rate is $112 per night
(single or double occupancy) plus tax (total: $122.92). The hotel says that we
can mention Computer-Aided Verification (CAV) and get that rate through as far
as the night of July 14. Their phone number is 800-545-6285 (on the web:
http://www.milleniumhotels.com).
http://www-housing.colorado.edu/conferences/map_trans.html
One can follow links from that page to find transportation options from the Denver airport. Two such options appear to be as follows.
http://www.supershuttle.com/htm/cities/dia.htmhttp://www.rtd-denver.com/skyRide/skyrtable.htmWe invite papers on any topic related to ACL2, including but not limited to:
We are looking for papers of no more than about 20 pages in length. Papers of at most about 5 pages will generally be considered for "short talks" (probably 20 or 25 minutes), and others will be considered for "long talks" (probably 30 or 40 minutes). However, authors are encouraged to state explicitly their preference for giving a short or long talk. Note that short talks may report on work in progress, challenge problems, clever tricks, and so on.
Papers will be refereed by members of the Program Committee.
Submissions should be sent by email to Matt Kaufmann (matt.kaufmann@amd.com) in
Postscript and/or PDF format. Papers that describe successful uses of ACL2
should be accompanied by ordinary text files containing the appropriate ACL2
input and instructions for how to process them with ACL2, although the papers
themselves should be self-contained.
We expect that accepted papers (both full and short) will be presented at the workshop and published in a conference proceedings format, perhaps on-line. Final copies of the papers will be collected shortly after the meeting.
Supporting materials. Where applicable, we encourage authors of accepted papers to provide ACL2 script files or ``books'' to provide full details, which can be mirrored on the ACL2 home page (above) and included in future ACL2 distributions. Please see the instructions for supporting materials.
| Submission Deadline | April 8, 2003 [extended from original date of April 1] |
| Acceptance Notification | May 8, 2003 [extended from original date of May 1] |
| Last day to send in registration without late fee | June 1, 2003 |
| Final Papers Due | July 7, 2003 |
| Workshop | July 13-14, 2003 |
| Sunday, July
13: Workshop, Day 1 | ||
| 8:30 | Breakfast | |
| 9:00 | Welcome | |
| 9:10 | Matt Kaufmann | A Tool for Simplifying Files of ACL2 Definitions [PDF] [PS] [Supporting materials] (Slide handouts: [PDF] [PS]) (Slides (full-size): [PDF] [PS]) |
| 9:40 | Joe Hendrix | Matrices in ACL2 [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 10:00 | Panagiotis Manolios Daron Vroon (speaker) |
Ordinal Arithmetic in ACL2 [PDF] [PS] |
| 10:30 | Long break (refreshments) | |
| 11:10 | Matyas Sustik | Proof of Dickson's Lemma Using the ACL2 Theorem
Prover via an Explicit Ordinal Mapping [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 11:40 | John Cowles (speaker), Ruben Gamboa, Jeff Van Baalen |
Using ACL2 Arrrays to Formalize Matrix Algebra [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 12:00 | Ruben Gamboa (speaker), John Cowles, Jeff Van Baalen |
On the Verification of Synthesized Kalman Filters [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 12:30 | Lunch | |
| 14:30 | Olga Shumsky Matlin (speaker), William McCune |
Encapsulation for Practical Simplification Procedures [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS] [PowerPoint]) |
| 14:50 | Rob Sumners | Fair Environment Assumptions in ACL2 [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 15:10 | Diana Toma (speaker), Dominique Borrione |
SHA Formalization [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 15:30 | Long break (refreshments) | |
| 16:10 | David Greve, Matthew Wilding (speaker), W. Mark Vanfleet |
A Separation Kernel Formal Security Policy [PDF] [PS] [Supporting materials] |
| 16:40 | Matt Kaufmann, J Moore |
What's new in ACL2; General Discussion (e.g., ACL2
enhancement requests) [Talk notes (plain text)] |
| 18:00 | End of first day | |
| Monday, July
14: Workshop, Day 2 | ||
| 8:30 | Breakfast | |
| 9:00 | Announcements | |
| 9:10 | J Strother Moore | Memory Taggings and Dynamic Data Structures [PDF] [PS] [Supporting materials] |
| 9:40 | J Strother Moore | Inductive Assertions and Operational Semantics -- Long Version [PDF] [PS] [Supporting materials] |
| 10:10 | Short break | |
| 10:25 | David Greve (speaker), Matthew Wilding |
Typed ACL2 Records [PDF] [PS] [Supporting materials] |
| 10:45 | David Greve (speaker), Matthew Wilding |
Using MBE to Speed a Verified Graph Pathfinder [PDF] [PS] [Supporting materials] |
| 11:05 | Long break (refreshments) | |
| 11:35 | Hanbing Liu | A Solution to the Rockwell Challenge [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS])) |
| 12:05 | Tao Song (speaker), Jim Alves-Foss, Calvin Ko, Cui Zhang, Karl Levitt |
Using ACL2 to Verify Security Properties of Specification-based Intrusion Detection Systems [PDF] [PS] [Supporting materials] |
| 12:25 | Lunch | |
| 14:25 | Julien Schmaltz, Ghiath Al Sammane, Dominique Borrione, Pierre Ostier, Diana Toma (speaker) |
Combining ACL2 and Mathematica for the Symbolic Simulation of Digital
Systems [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 14:45 | Julien Schmaltz (speaker), Dominique Borrione |
Validation of a parameterized bus architecture using ACL2 [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS]) |
| 15:05 | Short break | |
| 15:20 | Ruben Gamboa (speaker), Mark Patterson |
Polymorphism in ACL2 [PDF] [PS] (Slides: [PDF]) |
| 15:50 | Ruben Gamboa | Writing Literate Proofs with XML Tools [PDF] [PS] [Supporting materials page] (Slides: [PDF]) |
| 16:10 | Long break (refreshments) | |
| 16:40 | Sandip Ray (speaker), John Matthews, Mark Tuttle |
Certifying Compositional Model Checking Algorithms in ACL2 [PDF] [PS] [Supporting materials] (Slide handouts: [PDF] [PS]) (Slides (full-size): [PDF] [PS]) |
| 17:10 | Vernon Austel | Implementing abstract types in ACL2 [PDF] [PS] [Supporting materials] (Slides: [PDF] [PS (gzipped)]) |
| 17:30 | General Discussion (ACL2 enhancements, time/place of next workshop) | |
| 18:00 | Workshop ends | |
hunt@cs.utexas.edu)
matt.kaufmann@amd.com)
moore@cs.utexas.edu)
| Austel, Vernon | IBM |
| Cowles, John | Univ. of Wyoming |
| Fedeli, Andrea | St.com |
| Gamboa, Ruben | Univ. of Wyoming |
| Greve, Dave | Rockwell Collins |
| Harrison, John | Intel |
| Hendrix, Joe | Univ. of Illinois at Urbana-Champaign |
| Hunt, Warren | Univ. of Texas at Austin |
| Kaufmann, Matt | AMD |
| Kuzmina, Nadya | Univ. of Wyoming |
| Legato, Wilfred | U.S. Govt. |
| Liu, Hanbing | Univ. of Texas at Austin |
| Manolios, Pete | Georgia Tech Univ. |
| Matlin, Olga Shumsky | Argonne National Labs. |
| Moore, J | Univ. of Texas at Austin |
| Patterson, Mark | Univ. of Wyoming |
| Ray, Sandip | Univ. of Texas at Austin |
| Reeber, Erik | Univ. of Texas at Austin |
| Richards, Ray | Rockwell Collins |
| Roach, Steve | Univ. of Texas at El Paso |
| Schmaltz, Julien | TIMA Laboratory, Grenoble, France |
| Smith, Eric | AMD / Stanford Univ. |
| Song, Tao | Univ. of California at Davis |
| Sumners, Rob | AMD |
| Sustik, Matyas | Univ. of Texas at Austin |
| Toma, Diana | TIMA Laboratory, Grenoble, France |
| Van Groningen, Serita | Rockwell Collins / Univ. of Texas at Austin |
| Vroon, Daron | Georgia Tech Univ. |
| Wilding, Matthew | Rockwell Collins |