This course is about using logic and theorem proving to specify and verify software. It builds on the design recipe from How to Design Programs. We will use an interactive theorem prover called ACL2.
| Instructor: | Dale Vaillancourt | ||
| Office Hours: | Mon | 12:00 - 1:00 pm | 308 WVH |
| or stop by anytime during the week. | |||
| Classes: | Tue | 8:30 - 9:30 am | 164 WVH |
| Fri | 3:30 - 4:15 pm | 164 WVH | |
Tuesday meetings will be mostly lectures, and Friday meetings will work like more of a lab / recitation / studio depending on the week. We do not have a dedicated lab space for the course, so please bring your laptops with the course software installed on Fridays. One laptop per pair is sufficient if some of you do not wish to carry yours around.
We will use a theorem proving system called ACL2 and a development environment for it called Dracula. Look at the Dracula homepage for installation instructions.