Homepage: http://www.cs.utexas.edu/users/hunt/class/2021-fall/cs389r/cs389r.html
Homework will generally be assigned every week on Tuesday, and usually it is due nine days later on Thursday by the beginning of class. Of course, you may bring finished homework to class; otherwise, you must get it to the class TA before the due date and time. Remember, late homework is not accepted, but the lowest homework grade will be dropped. Assignments will appear here as the semester progresses. Please show your work -- partial credit cannot be awarded if only an incorrect answer is given. Homework will generally be submitted on Canvas, but if homework is turned in to the TA, it must have a cover sheet attached to the front. Only write the information requested on this cover sheet; do not include your Taxpayer ID number.
If you think that since you can drop one homework assignments, that it's OK to skip a homework, you are mistaken. In the body of homework assignments, various topics will be discussed. It is expected that even if you do not turn in a homework assignment, that you are familiar with the material discussed or referenced in the assignment itself. Thus, you are responsible for understanding and being able to use the concepts embodied in the homework assignments -- even if you don't turn in various homework assignments.
NOTE: The most accurate indicator of what grade a student will receive is their grades on homework assignments. Students that do and submit all of the homework generally out perform students that are lax about their homework. In this class, what you learn will be directly related to the effort you put forward on the homework and programming assignments.
You may discuss the homework questions with your peers, but the end product that you turn in should be your own work. We want you to learn with and from your peers, but each of you is responsible for your own work.
Thoughts About the CS389r Course Project
Project Proposal Pro-forma
One Slide
Title of Project
(e.g.) A Proof that Model M has the interesting property P.
Short Abstract -- Bullet point list
What will you be modeling in ACL2? What will you prove?
What is your connection to this application domain?
Some Interesting Display
Any Graphics or Equational Displays that can help others
``picture'' what your project is about. For example, a Diagram
of some digital circuit that you wish to analyze. Equation of
the main theorem you seek to prove.
One Page Proposal
Title of Project
(e.g.) A Proof that Model M has the interesting property P.
Background
What is the context (problematic situation) that you are
investigating in this project? What will you prove?
Why is ACL2 a good tool to use in working on this problem?
What is your connection to this technical area?
Technical Approach
What is your approach to the problem you are addressing? What
are the key steps in your technical workplan? Why do you think
that this work can be done in 1 month? (Oct 18 - Nov 18)
References
List of information sources you used in your project.
Some Interesting Displays
Any Graphics or Equational Displays that can help a reader
``picture'' how you have formulated and executed your approach.
Some diagram or architecture chart. Equation of the main
theorem you seek to prove. Your readers are likely ACL2 savvy,
so some key ACL2 code you will use to define your model.