What to do in advance of the workshop if you have time:
- Get a copy of ACL2 from github on your laptop and
build an
ACL2 executable, preferably based on CCL.
- Read :DOC
system-development and its subtopics, except perhaps for
subtopic VERIFY-GUARDS-FOR-SYSTEM-FUNCTIONS.
- Skim the agenda.
- Download and extract the examples
tarball,
examples.tgz
, which
contains the examples and exercises mentioned in that agenda.
- This workshop is for experienced ACL2
users. In particular, we assume that you are familiar
with stobjs
and that you can quickly get up to speed
on ruler-extenders,
since these are used in examples.
Back to Developer's Workshop page