 |
 |
||
|
|
|
|
 |
 |
|
|
|
|
|
 |
 |
|
|
|
|
|
 |
||
|
|
||
 |
15-414 Bug Catching: Automated Program Verification and Testing Fall 2007 Semester Computer Science Department |
Course Description
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.
Announcements
Dec 11, 2007: Information on HW8 has been updated. Please see this.
Nov 26, 2007: Michael's last two office hours (Nov 27 and Dec 4) will happen after class.
Oct 30, 2007: Note the change in Michael's office hours.
Lectures
Tuesdays and Thursdays from 3:00-4:20pm in Wean Hall Rm 5312.
Contact Information
| 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: Thursdays after class or by appointment |
| Teaching Assistant:
Michael Carl Tschantz
Office: Doherty Hall Rm 4301H E-mail: mtschant AT cs DOT cmu DOT edu Phone: 412-268-7375 Office hours: Tuesdays after class 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 |