15-414 Bug Catching: Automated Program Verification and Testing Fall 2006 Semester Computer Science Department

This course is about finding and preventing logical errors in concurrent systems, e.g., programs, hardware devices,controllers.  Though formal analysis requires understanding of many theoretical issues, the focus of this course will be on using practical verification tools to analyze interesting examples.  We will cover just enough theory to use the tools effectively and understand the examples.  The assignments will involve using some type of verification tool to find bugs in interesting designs.  We do not assume any prior knowledge of computer hardware, however, students who know hardware will find these techniques to be very useful.

Oct 11, 2006: Midterm on October 17, 2006 in class

Sep 5, 2006: Course webpage up. We will use blackboard for discussion and storing grades.

Classes T, Th 3:00 - 4:20 pm Wean Hall Rm 5310

Professor: Edmund M. Clarke Office: Wean Hall Rm 7117 E-mail: emc AT cs DOT cmu DOT edu Phone: (412) 268-2628    Fax: (412) 268-5576  Office hours: After class or by appointment

Teaching Assistant: Himanshu Jain Office: WeH 4112 E-mail: hjain AT cs DOT cmu DOT edu Phone: (412) 268-3047 Office hours: Friday 2-3pm or by appointment

Course Secretary: Denny Marous Office: Wean Hall Rm 7116 E-mail: dcm AT cs DOT cmu DOT edu Phone: (412) 268-7660 Fax: (412) 268-5576