ACL2 stands for ``A Computational Logic for Applicative Common Lisp'' but our research group is interested in all aspects of mechanized theorem proving and in the mechanized verification of hardware and software.
For spring semester 2017, ACL2 seminars are scheduled to take place on Fridays 10:15 am - 12:00 noon, in room GDC 7.808 (University of Texas at Austin).
This page lists meetings back to the start of the 2002-2003 academic year.
notes.org(slides for Emacs org-mode)
fig1.png(first figure for the slides above)
fig2.png(secondfigure for the slides above)
2016-02-22-gfg.tar.xz(tarball for the materials listed above)
rtl/rel9library, which includes definitions and theorems for reasoning about bit vectors and floating-point operations.
matt.tgz, which extracts to a directory,
matt/, that contains all of the above (see instructions in the
defattachevent for supporting execution of constrained functions, sound modification of system code, and program refinement.
consp, as well as a definitional principle.
support.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.
email@example.com of time):
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''.
http://www.cs.utexas.edu/users/sustik/quantifier-elimination/for slides, papers and references.