Homepage: http://www.cs.utexas.edu/users/hunt/class/2008-fall/cs389r/cs389r.html
Unique Number: 55857
Class Room Number: Taylor Hall, 3.144
Class Time: Tuesday, Thursday, 12:30 to 1:50 pm
Reference Textbook: Computer-Aided Reasoning: An Approach
Textbook Authors: Kaufmann, Manolios, and Moore
Purchase Location: From Carol Hyink, Taylor Hall 2.116
Cost: $15 -- cash only
Instructor: Warren A. Hunt, Jr.
Office Location: Main 2014
Office Hours: Wednesday, 2:00 to 3:50 pm
E-mail: hunt@cs.utexas.edu
Co-Instructor: Sandip Ray
Office Location: Main 2004
Office Hours: By appointment
E-mail: sandip@cs.utexas.edu
Below is an approximate syllabus for the class. We may adjust the content to suit the interests of the class.
Aug 28 Introduction -- Recursion, Induction, so what? Sep 2 Using ACL2 for Modeling, Recursive Definitions Sep 4 Programming and modeling in ACL2 Sep 9 ACL2 Logic presentation, data types, terms Sep 11 Axioms, terms as formulas Sep 16 Function Definition Sep 18 Substitution, abbreviations Sep 23 Principle of Definition Sep 25 Induction Principle, Examples Sep 30 Proof Examples Oct 2 Catch up Oct 7 ACL2 System Demonstration (Matt Kaufmann) Oct 9 Low-level representation of Boolean formulas Oct 14 Boolean formula semantics Oct 16 Higher-level representation of Boolean formula Oct 21 Student project discussion Oct 23 Student project discussion Oct 28 General Induction Principle Oct 30 ACL2 System Usage (Matt Kaufmann) Nov 4 Quantification Nov 6 TBD Nov 11 HDL syntax and semantics Nov 13 HDL syntax and semantics * Nov 18 In-Class Exam Nov 20 TBD Nov 25 Exam discussion Nov 27 Thanksgiving holiday Dec 2 Student Presentations Dec 4 Student Presentations
Return to CS389r course homepage.