Seminars may take place on Wednesdays 4:00-5:45 pm in ACES 3.116, University of Texas. This page lists meetings back to the start of the 2002-2003 academic year.
defattach event for supporting execution of constrained
functions, sound modification of system code, and program
refinement.defsort book.if, car,
cdr, cons, and consp, as well as a
definitional principle.clock-to-trad.lispdefinition.lispcontradiction.lispsupport.tar.gz [all of the above]
make-event,
which provides the capability to do something like macro-expansion but with access
to the ACL2 state and logical world.http://www.cis.upenn.edu/group/proj/plclub/mmm/.
They will also discuss some macros for ACL2 based on ideas from Haskell.
if-tautologyp.
kaufmann@cs.utexas.edu ahead of
time):http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/whats-new/talk.txt.
I will talk briefly about staged simplification. Several years ago Pete Manolios and J introduced the notion of stable-under-simplificationp to control rewriting expressions involving a large and detailed machine. Since then, I have found that there is great benefit to be derived by enabling (and subsequently disabling) nonlinear arithmetic under similar control. Both of these are related to the common strategy of examining a failed proof and giving hints at the ``checkpoints''.
go-to-node.tar.gz
http://www.cs.utexas.edu/users/sustik/quantifier-elimination/
for slides, papers and references.
- 8/13/03, Fares Fraij
Fares will talk about his experiences with ACL2 from the perspective of a new user.
- 8/06/03, Robert Krug
Robert will continue talking about how to write a library of arithmetic books.
- 7/30/03, Robert Krug
Robert will continue talking about how to write a library of arithmetic books.
- 7/23/03, Robert Krug
Robert will continue talking about how to write a library of arithmetic books.
- 7/16/03, Robert Krug
How to write a library of arithmetic books.
- 7/02/03, Joe Hendrix
An overview of Maude
Slides
[PDF]
[PS]
Maude input files:
- 6/25/03, Joe Hendrix
The new Java memory models, continued
Slides [Postscript] (same as last week's)
- 6/18/03, Joe Hendrix
The new Java memory models
Slides [Postscript]
- 6/11/03, Robert Krug
Some work with ACL2 and arithmetic
Abstract
- 6/04/03, Matyas Sustik
Matyas will talk on his proof of Dixon's Lemma in ACL2
Abstract
See Matyas's home page for a link to get to the slides.
- 5/28/03, Hanbing Liu
Hanbing will give a talk based his paper with J Moore,
"Executable JVM Model for Analytical Reasoning: A Study"
Abstract
The paper (PS)
- 5/21/03, Matt Kaufmann
Dealing With Prover Heuristics in ACL2: A Case Study
Talk notes
NOTE: This will be a short talk. Most of the meeting will consist of an
extended round-table discussion, perhaps with a focus on upcoming summer
projects.
- 4/30/03, Qiang Zhang
Qiang will complete his 4/16 talk on compiler verification.
Also, we will figure out the summer schedule.
- 4/23/03, J Moore
J Moore will talk about about partial functions in ACL2:
2000 ACL2 Workshop paper (P. Manoilios, J Moore)
[PDF]
[PS]
[Supporting Materials]
- 4/16/03, Qiang Zhang
[Qiang will talk on his work on compiler verification.]
- 4/09/03, John Erickson
Generalizing Finite Cases
Abstract
- 4/02/03
No seminar, but people are encouraged to attend the following colloquium talk:
TAY 3.128, 4:00 pm (coffee at 3:30)
Steven M. German, IBM T.J. Watson Research Center
Experiences in Formal Design and Verification of Cache Memory
- 3/26/03, Rob Sumners
Continuation of preceding week's talk
Slides [Postscript] (same as last week's)
- 3/19/03, Rob Sumners
A New Simplifier
Slides [Postscript]
- 3/12/03, no seminar (spring break)
- 3/05/03, Sandip Ray
Continuation of preceding week's talk
[See just below for slides etc.]
- 2/26/03, Sandip Ray
Continuation of preceding week's talk
[See just below for slides etc.]
- 2/19/03, Sandip Ray
Continuation of preceding week's talk
[See just below for slides etc.]
- 2/12/03, Sandip Ray
Verification of model-checking reductions at CRL
Abstract
Slides [HTML]
Slides [Postscript; printing works, but viewing may not work]
.lisp file
Also, Matt Kaufmann will talk briefly about recent changes in rewriting under induction.
- 1/29/03, no speaker
Extended round-table discussion
- 1/22/03, Erik Reeber
Review of work of Praxis Critical Systems
Abstract
Slides
- 1/15/03
Extended round-table discussion.
NOTE: If time, Matt Kaufmann will discuss:
Proposal for attaching executable functions to
logic definitions.
Matt will also mention
Avoiding infinite loops in the ACL2
rewriter.
- 12/04/02, Bill Young
Review of "Transformation-Oriented Programming:
A Development Methodology for High Assurance Software"
by Victor Winter, Steve Roach, Greg Wickstrom.
[J asked Bill to look at
this to assess whether ACL2 could somehow be used in this context.]
- 11/20/02, Shant Harutunian
Continuation of preceding week's talk (Note: slides have been further updated.)
- 11/13/02
- J Moore
Short discussion on how to structure his upcoming JVM class
- Shant Harutunian
Continuation of preceding week's talk (Note: slides have been updated.)
- 11/06/02, Shant Harutunian
Model-Checking in Dense Real Time
Abstract [plain text]
Slides [PDF]
- 10/30/02, no speaker
Extended round-table discussion
- 10/23/02, Robert Krug
Continuation of preceding weeks' talks
- 10/16/02, Robert Krug
Continuation of preceding week's talk
- 10/9/02, Robert Krug
Arithmetic in ACL2
Abstract [plain text]
- 10/2/02, Robert Krug
ACL2 Basics
Abstract [plain text]
- 9/25/02, Hanbing Liu
Continuation of preceding week's talk
Abstract [plain text]
- 9/18/02, Hanbing Liu
Introduction to ACL2 JVM Models
Abstract [plain text]
Slides
[PDF]
[PPT]
- 9/11/02, Vinod Viswanath
Assertion Based Verification of Hardware Circuits
Abstract [plain text]
Slides [PDF]
- 9/4/02
- Robert Krug
Brief talk on break-rewrite
- Michael "Bogo" Bogomolny
Paper review: "Little Engines of Proof", by N. Shankar
Shankar's paper [PDF]
Shankar's slides [PDF]
- 8/28/02, Matt Kaufmann
A Tool for Simplifying Files of Definitions
Abstract [plain text]
Handout [plain text]