coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ACL2-2003 workshop (CAV'03 satellite event)

From: "Matt Kaufmann" <matt.kaufmann AT amd.com>
To: acl2 AT lists.cc.utexas.edu, categories AT mta.ca, colt AT cs.uiuc.edu, concurrency AT cwi.nl, coq-club AT pauillac.inria.fr, elf-list AT cs.cmu.edu, formal-methods AT cs.uidaho.edu, forum AT jsoftware.com, fsdm AT it.uq.edu.au, IFIP-WG1_3-Members AT brics.dk, imps AT linus.mitre.org, info-hol AT ultimate.cs.byu.edu, isabelle-users AT cl.cam.ac.uk, isss-people AT ics.uci.edu, lics AT research.bell-labs.com, logic-list AT cs.rice.edu, lotos-na AT site.uottawa.ca, lprolog AT cs.umn.edu, mizar-forum AT mizar.uwb.edu.pl, nuprlnotes AT cs.cornell.edu, papm AT dcs.ed.ac.uk, pvs AT csl.sri.com, qed AT mcs.anl.gov, rewriting AT ens-lyon.fr, theorem-provers AT ai.mit.edu, zforum AT prg.ox.ac.uk
Subject: [Coq-Club] ACL2-2003 workshop (CAV'03 satellite event)
Date: Tue, 20 May 2003 14:23:32 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Greetings [and apologies if you get multiple copies]:

The deadline for registering for the July 13-14 ACL2 workshop without a late
fee is June 1.  Some information is below.  For more information, including a
list of talks, see: http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.

.....

The next ACL2 Workshop will be held July 13-14, 2003, in Boulder, Colorado,
USA, in conjunction with (and immediately following) CAV'03.  We invite users
of ACL2, users of other theorem provers, and persons interested in the
applications of theorem proving technology to attend.

ACL2 is a state-of-the-art automated reasoning system, which 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 the presentation and discussion of projects using ACL2 as well as the
evolution of the tool.  Topics include the following.

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

[Coq-Club] ACL2-2003 workshop (CAV'03 satellite event), Matt Kaufmann