ACL2

Department of Computer Sciences

1999 ACL2 Workshop

March 29 - March 31, 1999

This page is current as of June 7, 1999.
Update: The proceedings have been published as this book.

Information for attendees

Action Items

The workshop will take place at the University of Texas at Austin in the Texas Governor's Room of the Texas Union (located on the third level of the Texas Union).

We have sent email to all participants regarding carpooling and parking. Recall that the parking permits are available from the guard at 24th and Whitis.

We have prepared a map for attendees.
An interactive map (from yahoo) centered at Taylor Hall (2400 Guadalupe, Austin, TX) is available.
Finally, more extensive online campus maps are also available.

Computing resources will be available in Taylor Hall.
We will have an LCD projector.

Local pointers

List of participants and presentations

Participant Title of Talk
Ken Albin Memory Models?
Nina Amla Not presenting
Vernon Austel The ACL2 model used for the FIPS level 4 evaluation of the IBM 4758 secure coprocessor
Piergiorgio Bertoli Proving the correctness of an Embedded Verifier for a Safety-Critical translator
Michael N. Bogomolny Not presenting
Dominique Borrione Using macros to mimic VHDL in ACL2
Bob Boyer Not presenting
John Cowles Knuth's Generalization of McCarthy's 91 Function
Arthur Flatau Not presenting
Jeff Ford Not presenting
Ruben Gamboa Continuity and Differentiability in ACL2?
Philippe Georgelin Using macros to mimic VHDL in ACL2
Wolfgang Goerigk Verified Result Checking for Safety of an Automatic Test Plan Generator
David Greve Suggested ACL2 Enhancements
Warren Hunt Dual-Eval in ACL2
Damir Jamsek Symbolic Trajectory Analysis?
Matt Kaufmann The Application of a Modular Proof Methodology for ACL2 to Proving the Fundamental Theorem of Calculus
Robert Krug Not presenting
Bill Legato Not presenting
Pete Manolios Mu-Calculus Model-Checking in ACL2
William McCune Proof Checker for First Order Logic
J Moore Single-Threaded Objects
Michael Permana Not presenting
Frank Rimlinger Not presenting
David Russinoff Mechanical Verification of Register-Transfer Logic: A Floating-Point Multiplier
Jun Sawada Verifying A Simple Pipelined Machine Model
Bill Schelter The State of GCL
Rob Sumners Not presenting
Matt Wilding Single-Threaded Processor Models: Enabling Proof and High-Speed Execution
Bill Young Not presenting

Schedule of events

A "?" after a title means that we have not received a title from the speaker (we just made up titles in this case). If we received an abstract, then you can click on the title to see the abstract.

Monday, March 29, 1999

Time Speaker Title
8:00-8:30 J Moore
Matt Kaufmann		 Welcome, Breakfast
8:30-9:30 Warren Hunt Dual-Eval in ACL2
9:30-10:00 Dominique Borrione
Philippe Georgelin		 Using macros to mimic VHDL in ACL2
10:00-10:30 Damir Jamsek Symbolic Trajectory Analysis?
10:30-11:00   Break
11:00-11:45 Vernon Austel The ACL2 model used for the FIPS level 4 evaluation of the IBM 4758 secure coprocessor
11:45-2:00   Lunch
2:00-2:30 Bill Schelter The State of GCL
2:30-5:00 David Russinoff Mechanical Verification of Register-Transfer Logic: A Floating-Point Multiplier
5:00-5:15 Discussion Planning for dinner, miscellaneous
7:00-9:30   Dinner at Fonda San Miguel

Tuesday, March 30, 1999

Time Speaker Title
8:00-8:30 J Moore Welcome, Breakfast
8:30-9:15 Piergiorgio Bertoli Proving the correctness of an Embedded Verifier for a Safety-Critical translator
9:15-9:45 Wolfgang Goerigk Verified Result Checking for Safety of an Automatic Test Plan Generator
9:45-11:00 J Moore Single-Threaded Objects
11:00-11:15   Break
11:15-12:15 Matt Wilding Single-Threaded Processor Models: Enabling Proof and High-Speed Execution
12:15-1:15   Lunch
1:15-2:15 Jun Sawada Verifying A Simple Pipelined Machine Model
2:15-2:45 Ken Albin Memory Models?
2:45-3:45 David Greve Suggested ACL2 Enhancements
3:45-4:30 Discussion Changes to ACL2
4:30-5:00 David Greve
Matt Wilding		 JEM1 Model Demonstration

Wednesday, March 31, 1999

Time Speaker Title
8:00-8:30 J Moore Welcome, Breakfast
8:30-9:30 William McCune Proof Checker for First Order Logic
9:30-10:30 Pete Manolios Mu-Calculus Model-Checking in ACL2
10:30-11:00   Break
11:00-12:00 John Cowles Knuth's Generalization of McCarthy's 91 Function
12:00-1:30   Lunch
1:30-2:30 Ruben Gamboa Continuity and Differentiability in ACL2?
2:30-3:30 Matt Kaufmann The Application of a Modular Proof Methodology for ACL2 to Proving the Fundamental Theorem of Calculus
3:30-4:30 Discussion Planning for the next ACL2 Workshop, Changes to ACL2