ACL2 Workshop 2000 (Reminder)

[Matthew Kaufmann]

******************************************************************************
COLT MAILING LIST  (colt@cs.uiuc.edu)   The following message was received 
for distribution to subscribers of the colt mailing list.
******************************************************************************
[We apologize if you receive multiple copies of this message]

Hello --

ACL2 Workshop 2000 is open to all and will be held October 30-31, 2000 (brief
tutorial on Oct 29), just before FMCAD and (also) in Austin, Texas.  The
original invitation is included below (with one new program committee member
added).  In a nutshell: please pre-register as soon as possible if you are
interested in attending, and note the submission deadline of July 15, 2000.
Details (including a form to return) are included below.

Regards,
Matt Kaufmann and J Moore

ACL2 Workshop 2000
University of Texas at Austin
Austin, Texas
Oct 30-31, 2000; brief tutorial afternoon of Oct 29.

The next workshop on the ACL2 theorem prover and its applications will
be held at the University of Texas on Monday and Tuesday, October
30-31, 2000.  Immediately after the ACL2 workshop, Austin hosts the
Formal Methods in Computer-Aided Design (FMCAD) conference.  It will
be easy to attend both.

ACL2 is described at http://www.cs.utexas.edu/users/moore/acl2.  Last
year's workshop produced two books,

* Computer-Aided Reasoning: An Approach, Kaufmann, Manolios, Moore,
  Kluwer, (May, 2000)
* Computer-Aided Reasoning: ACL2 Case Studies, Kaufmann, Manolios, Moore
  (eds), Kluwer, (May, 2000)

and includes articles by a number of contributors on topics ranging
from real analysis and first-order logic to the mechanical
verification of designs of industrial interest like an RTL description
of a floating-point multiplier and the verification of a safety-
critical component of a compiler.

This year's ACL2 workshop is open to all.  If you would like to
attend, please let us know by filling out and returning the
pre-registration form below, so we can arrange for an appropriately
large meeting room.

For those who don't know ACL2 but wish to learn enough to listen to
the talks and see what's going on in the ACL2 community, we will
present a brief tutorial on Sunday afternoon before the meeting.

There will be a nominal registration fee to cover the cost of food,
the meeting room and, we expect, the proceedings, to be produced and
mailed after the meeting.  We anticipate the fee being around $100
and will give full details when the details have been finalized.
The fee will be collected by check or cash at the workshop.

CALL FOR PAPERS

We invite papers on any topic related to ACL2, including but not
limited to:

  * applications of the theorem prover
  * improvements and extensions to the theorem prover
  * comparisons of ACL2 to other theorem provers,
     programming languages, or specification languages
  * solved challenge problems for ACL2 users (especially
     challenges that help newcomers learn the system)
  * implementations connecting ACL2 and other systems

You should assume that the audience has a working knowledge of ACL2,
including familiarity with the syntax, the basic commands, and
modeling techniques used.

We are looking for two kinds of papers.

  * Full papers: no more than about 20 pages in length.
  * Short papers: at most five pages, these may report on work in
    progress, challenge problems, clever tricks, etc.

Full papers will be reviewed by the program committee (below); short
papers will be reviewed by a subset of the committee.

Submissions should be sent by email in Postscript format, when
possible.  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.
Final copies of the papers will be collected shortly after the October
meeting.  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.

PROGRAM COMMITTEE:
Bob Boyer           (CS Department, University of Texas, Austin, Texas)
Piergiorgio Bertoli (IRST - Istituto per la Ricerca Scientifica e Tecnologica,
                     Povo, Italy)
John Cowles         (CS Department, University of Wyoming, Laramie, Wyoming)
Wolfgang Goerigk    (IIPM, Christian-Albrechts-Universitat zu Kiel, Germany)
Matt Kaufmann       (Advanced Micro Devices, Inc., Austin, Texas)
Pete Manolios       (CS Department, University of Texas, Austin, Texas)
William McCune      (MCS, Argonne National Laboratory, Argonne, Illinois)
J Moore             (CS Department, University of Texas, Austin, Texas)
David Russinoff     (Advanced Micro Devices, Inc., Austin, Texas)
Jun Sawada          (IBM Austin Research Laboratory, Austin, Texas)
Matt Wilding        (ATC, Rockwell Collins, Inc., Cedar Rapids, Iowa)


ORGANIZING COMMITTEE:
  Matt Kaufmann     (matt.kaufmann@amd.com)
  J Moore           (moore@cs.utexas.edu)

DATES:
  Pre-Registration          as soon as possible
  Submission Deadline:      July 15, 2000
  Acceptance Notification:  September 1, 2000
  Workshop:                 October 30-31, 2000 (brief tutorial on Oct 29)


---------------------------------------------------------------------------
ACL2 Workshop 2000 -- Pre-Registration Form

Please fill out and return this form to jomoore@cs.utexas.edu.  By doing so
you can help us make suitable arrangements for the workshop.  Fees will
be collected only if you attend the workshop.


Name:    ________________________
email:   ________________________
Address: ________________________
         ________________________

Check those that apply.

[]  I hope to submit a long paper.
[]  I hope to submit a short paper.
[]  I plan to attend the ACL2 tutorial session, Sunday afternoon,
      October 29, 2000.
[]  I plan to attend the workshop dinner, Sunday evening, 
      October 29, 2000 (and pay for it at the time).
[]  I plan to attend the workshop, Monday and Tuesday,
      October 30-31, 2000.
[]  I would like a UT parking permit October 30-31, 2000.
[]  I am a student at ____________.

I understand that if I attend the workshop I will be expected to pay a
registration fee (by cash or check) during the workshop to cover
workshop costs.  The exact amount of the fee will be announced to the
registrants several weeks before the workshop.  Students will receive
a 25% discount.

You will be responsible for your own hotel/accommodation arrangements.
FMCAD 2000 is being held at the Austin Marriot Hotel at the Capitol,
Nov 1-3.  Expecting overlap between those attending our workshop and
FMCAD, the hotel has agreed to give us some ``early arrival'' rooms
starting Saturday, October 28, at the FMCAD rate.  Please contact the
hotel directly (512 478-1111) and mention ``FMCAD.''  The rate is $149
per night (for a single or for a double).

Tee-Shirts:

The ACL2 Workshop tee-shirt has the ACL2 ``infinity'' logo on the
front and ``ACL2 Workshop 2000'' and a slogan on the back.

I will probably buy some ACL2 Workshop 2000 tee-shirts.  Each will
cost about $11, payable by cash or check at the workshop.

Number in each size: Small    Med    Large   X-Large  XX-Large
                      ___     ___     ___     ___     ___

Preference Poll:

We will produce a fixed number of shirts in each of one or two colors.
What is your preference?

[] a dark color (e.g., black, navy)
[] a light color (e.g., white, light blue)
[] a bright color (e.g., red, yellow)

Slogan suggestion:

________________________

(Last year's slogan was:  ``It ain't over til the last Q.E.D.'')