1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
<HTML>
<HEAD><TITLE>ACL2 Workshops and UT ACL2 Seminar</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
<H1>The <A HREF="http://www.cs.utexas.edu/users/moore/acl2/index.html">ACL2</A> Workshop Series</H1>
We hold regular workshops. In 2010, the ACL2 Workshop did a one-time
merger with TPHOLs to form the first International Conference on
Interactive Theorem Proving (ITP). Such a merger may occur again, but
whether or not that happens, the ACL2 community is encouraged to
participate in ITP. Other conferences of particular interest to the
ACL2 community include CAV (Computer Aided Verification)
and <A HREF="http://www.cs.utexas.edu/users/hunt/FMCAD/">FMCAD</A>
(Formal Methods in Computer Aided Design).
<p>
<UL>
<LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2015/index.html">ACL2
Workshop 2015</A>: October 1-2, 2015, Austin, Texas, USA.
(Co-located with <A HREF="http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD15/index.shtml">FMCAD 2015</a>.)</LI>
<LI><A NAME="2014"></A><A HREF="http://vsl2014.at/acl2/">ACL2 Workshop 2014</A>: July 12-13, 2014, Vienna, Austria,
as an ITP-affiliated workshop of FLoC (part of the
<a href="http://vsl2014.at/">Vienna Summer of Logic</a>).
<ul>
<li><a href="http://cs.ru.nl/~freekver/acl2_14_program.html">Slides</a></li>
<li><a href="http://arxiv.org/html/1406.1238v1">Proceedings</a></li>
</ul>
</LI>
<LI><A HREF="http://www.cs.uwyo.edu/~ruben/acl2-13">ACL2 Workshop 2013</A>: May 30-31, 2013, University of Wyoming,
Laramie, Wyoming, USA.
<ul>
<li><a href="http://eptcs.web.cse.unsw.edu.au/content.cgi?ACL22013">Proceedings</a></li>
</ul>
</LI>
<LI><A HREF="http://www.cs.ru.nl/~julien/acl2-11/Home.html">ACL2
Workshop 2011</A>: November 3-4, 2011, Austin, Texas, USA.
(Co-located with <a
href="http://www.cs.utexas.edu/users/ragerdl/fmcad11/">FMCAD 2011</a>.)
<ul>
<li><a href="http://eptcs.web.cse.unsw.edu.au/content.cgi?ACL22011">Proceedings</a></li>
</ul>
</LI>
<LI><A HREF="http://www.cs.utexas.edu/users/kaufmann/itp-2010/">ITP 2010: Int'l Conference on
Interactive Theorem Proving (ITP) 2010</A>: July 11-14, 2010, Edinburgh,
Scotland; part of <A href="http://floc-conference.org">FLoC 2010</A>.<br>
<LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2009/">ACL2 Workshop 2009</A>: May 11-12, 2009, Boston, Massachusetts, USA.
(<a href=" http://portal.acm.org/citation.cfm?id=1637837&coll=GUIDE&dl=GUIDE&CFID=101915764&CFTOKEN=26521015">Proceedings available
from ACM Digital Library.</a>)</LI>
<LI><A HREF="http://www.cs.uwyo.edu/~ruben/acl2-07">ACL2 Workshop 2007</A>: November 15-16, 2007, Austin, Texas, USA.</LI>
<LI><A HREF="http://www.ccs.neu.edu/home/pete/acl206/">ACL2 Workshop
2006</A>: August 15-16, 2006, Seattle, Washington, USA. (<a href="http://portal.acm.org/toc.cfm?id=1217975&coll=portal&dl=ACM&type=proceeding&idx=SERIES10714&part=Proceedings&WantType=Proceedings&title=ACM%20International%20Conference%20Proceeding%20Series">Proceedings available
from ACM Digital Library.</a>)</LI>
<LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2004">ACL2 Workshop 2004</A>: November 18-19, 2004, Austin, Texas, USA.</LI>
<LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2003">ACL2 Workshop 2003</A>: July 13-14, 2003, Boulder, Colorado, USA.</LI>
<LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2002">ACL2 Workshop 2002</A>: April 8-9, 2002, Grenoble, France. </LI>
<LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2000">ACL2 Workshop 2000</A>: October 30-31, 2000, Austin, Texas, USA.</LI>
<LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-1999">ACL2 Workshop 1999</A>:
March 29-31, 1999, Austin, Texas, USA.</LI>
</UL>
<p>
Here is a list of past ACL2 Workshop slogans.
<ul>
<li>1999: It ain't over til the last Q.E.D.</li>
<li>2000: Just prove it.</li>
<li>2002: Accumulated Persistence</li>
<li>2003: No software too trivial. No error too obscure.</li>
<li>2004: Defun starts here</li>
<li>2006: ACM Software Systems Award Winner!</li>
<li>2007: Save the world. Use make-event.</li>
<li>2009: <i>None</i></li>
<li>2011: We aim to prove</li>
<li>2013: Pain is temporary; theorems are forever.</li>
<li>2014: I love the smell of parentheses in the morning.</li>
<li>2015: 25 years of rewriting history</li>
</ul>
<p>
Jared Davis has graciously supplied <a
href="http://www.cs.utexas.edu/users/jared/acl2/workshops-bibtex/">a listing of
bibtex entries for the 2000 through 2004 ACL2 workshops.</a>.
<p>
ACL2 input files (certifiable books) from the preceding workshops are available
from the links above. <b>WARNING</b>: The above links point to the original
versions of those books. In order to obtain up-to-date versions of those books
that will certify in
the <a href="http://www.cs.utexas.edu/users/moore/acl2/">latest
version of ACL2</a>, you should
<a
href="http://code.google.com/p/acl2-books/downloads">
download workshops.tar.gz</a> to the <CODE>acl2-sources/books/</CODE>
subdirectory of your ACL2 distribution, and then gunzip and extract it. On a
Unix/Linux system you can then certify all the books by standing in the
<CODE>acl2-sources/</CODE> directory and issuing the command
<CODE>make regression</CODE>.
<H1>ACL2 Seminar at UT</H1>
An ACL2 seminar meets regularly at the University of Texas. A list of past
talks, generally accompanied by abstracts and sometimes slides, may be found on
the <a href="http://www.cs.utexas.edu/users/moore/acl2/seminar/index.html">UT ACL2 seminar
page</a>.
<H1>ACL2 Course Materials</H1>
The links listed below will take you to materials for some courses
that involve ACL2. This list is loosely maintained and incomplete,
and is given in no particular order. We strongly encourage you to
send email to <A HREF="mailto:kaufmann@cs.utexas.edu">Matt
Kaufmann</A> and <A HREF="mailto:moore@cs.utexas.edu">J Strother
Moore</A> if you have additional such links to contribute.
<ul>
<li><a href="http://www.ccs.neu.edu/home/riccardo/courses/csu290-sp09/">CSU
290 Spring 2009</a> at Northeastern.
<li>The following two interfaces to ACL2 support the teaching of ACL2
to undergraduates:
<ul>
<li>The <a href="http://acl2s.peterd.org/acl2s/">ACL2 Sedan
(ACL2s)</a></li>
<li><a href="http://www.ccs.neu.edu/home/cce/acl2/">DrACuLa</a></li>
</ul>
<li>Here is a link to the <a
href="http://www.faculty.idc.ac.il/yishai/reasoning/">web
page for Yishai Feldman's Computer-Aided Reasoning course at The Interdisciplinary Center, Herzliya</a>.</li>
<li>John Cowles, <a href="http://www.cs.uwyo.edu/~cowles/jvm-acl2/">COSC5010:
Formalizing the JVM in ACL2</a>, Univ. of Wyoming.</li>
<li>Links to some of Warren Hunt's courses, many of which use ACL2, may be found <a
href="http://www.cs.utexas.edu/users/hunt/class/index.html">here</a>.</li>
<li><a
href="http://www.ccs.neu.edu/home/pete/courses/Logic-and-Computation/2008-Spring/">Logic
and Computation</a>, a freshman class taught by Pete Manolios and Riccardo
Pucella at Northeastern.</li>
<li>Here are links to web pages for courses taught by Pete Manolios at
Georgia Tech:
<ul>
<li><a href="http://www.cc.gatech.edu/~manolios/courses/Computational-Logic/2005-Spring/">CS 8803 Computational Logic
(Spring 2005)</a></li>
<li><a
href="http://www.cc.gatech.edu/fac/Pete.Manolios/courses/Hardware-Verification-Seminar/2004-Fall/">CS
8001 Hardware Verification Fall 2004</a></li>
<li><a href="http://www.ccs.neu.edu/home/pete/courses/Processor-design/2002-Fall/">CS 3220 Processor Design.</a></li>
</li>
</ul>
<li>Links to some of J Moore's courses, many of which use ACL2, may be found <a
href="http://www.cs.utexas.edu/users/moore/classes/index.html">here</a>.</li>
<li><a href="http://www.cs.ou.edu/~rlpage/SEcollab/">A course taught by Rex Page at the
Univ. of Oklahoma, and related links.</a></li>
<li><a href="http://www.stanford.edu/~ewsmith/acl2/">Eric Smith's web page for a class at Stanford</a></li>
</ul>
<BR><HR><BR><BR><BR><BR><BR><BR>
</BODY>
</HTML>
|
