CS G379 Decision Procedures for Verification
Fall 2007


Pete Manolios

Office hours:
WVH 332
by appointment

Class Information

Course number:
Web page:
CS G379
Wednesday 4:30PM-6:00PM in 366 West Village Bldg H
Exceptions: On 10/3, 10/17, 10/24, and 11/7 we will meet in Room 166 (same building)
Friday 3:25PM-5:05PM in 270 West Village Bldg F

The class is hosting the 1st Workshop on Decision Procedures for Verification. Check it out.

Class Web Pages

Homework Assignments



Course Description

This is a course on the state of the art in practical decision procedures for various fragments of logic arising in software and hardware verification. We will cover decision procedures for logics ranging from propositional logic to temporal logic to logics that include arithmetic, uninterpreted functions, equality, arrays, etc. We will also discuss abstraction, refinement, how to combine decision procedures, and the ACL2 theorem proving system.

Teaching Philosophy

My goal is to help you develop into critical, independent-thinking, and creative scientists. In this course, I will try to do this by giving you opportunities to grapple with and gain technical mastery of recent results in decision procedures. You gain technical mastery by doing and, for the most part, this occurs outside of the class. My role is to create the opportunity for learning; it is only with your active participation that learning truly takes place.

During lectures I try to explain, clarify, emphasize, summarize, encourage, and motivate. I can also answer questions, lead discussions, and ask questions. In class you have an opportunity to test your understanding, so things work best if you come to class prepared. We can then focus on the interesting issues, rather than on covering material that you could just as easily find in the readings.


If you have any questions, please come by and see me, call, or send email. My contact information appears above.

Last modified: Thu Sep 6 11:56:27 EDT 2007