ACL2 Theorem Proving Seminar at the University of Texas

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 fall semester 2014, ACL2 seminars will generally take place on Tuesdays 4:00 pm - 5:45 pm, in room GDC 7.808 (University of Texas at Austin). This page lists meetings back to the start of the 2002-2003 academic year.


Click here for some formal methods papers (for possible future presentations).

Upcoming meetings:

Note: meetings this semester (fall 2014) will generally start with about 15 minutes of discussion pertaining to booting FreeBSD on our x86 model, unless there is an outside speaker.

Previous meetings (reverse order):

Talks Preceding the 2002-2003 Academic Year

Examples and log from Recursion and Induction class Nov. 1, 2011