15-414 Bug Catching: Automated Program Verification and Testing
Fall 2011 SemesterComputer Science Department
Course Description
At some point in their careers, most CS and ECE students will develop software or hardware that must be ultra reliable. Logical errors in such designs can be costly, even life threatening. There has already been a number of well publicized errors like the Intel Pentium floating point error and the Ariane 5 crash. In this course we will study foundational concepts, and tools built on them, for finding and preventing such errors. We will cover some of the most prominent ideas in this important and evolving field -- including propositional satisfiability, Binary Decision Diagrams, model checking, abstraction, static analysis, abstraction-refinement, bounded model checking, and probabilistic model checking. We will also study some of the successful tools in this area. There will be emphasis on both the theoretical basis of these tools, as well as their hands-on use on real examples. This course can be used as one of the Fundamentals of Algorithms requirement.
Announcements
- 12/13 Statistics about Mid-term2 result
- The 2nd mid-term will be on December 9th from 3:00-4:30 pm @ GHC 4211.
- We will have a recitation on Partial Order Reduction.
- 12/02 Fri 3:00 - 4:30 PM @ GHC 4211
- 11/17 SPIN examples code [zip] is updated.
- 11/17 We will have a session to explain the nuclear project.
- 11/18 Fri 3:00 - 4:00 PM @ GHC 4405
- 11/14 We encourage students to write their own proposal for the final project (Due: 11/18).
- 11/14 The default project is out [pdf/templates] (Due: 12/14)
- 11/02 HW6 is out! (Due: 11/23)
- 10/26 HW5 is out! (Due: 11/09)
- We will have mid-term review sessions
- 10/26 Wed 5:30 - 6:30 PM @ GHC 8102
- 10/28 Fri 3:30 - 4:30 PM @ GHC 8102
- 10/24 Statistics about Mid-term result
- 10/10 A correction has been made to HW4
- 10/08 The mid-term exam will be on October 17th from 3:00-4:20 pm.
- 10/06 A correction has been made to HW4
- 10/05 HW4 is out! (Due: 10/26)
- 09/22 A correction has been made to HW3
- 09/21 HW3 is out! (Due: 10/5)
- 09/11 A correction has been made to HW2
- 09/08 HW2 is out! (Due: 9/21)
- 09/01 HW1 is out! (updated at 9/2) (Due: 9/14)
- 08/29 Welcome to 15414!
Lectures
Monday and Wednesday from 3:00 to 4:20 pm in GHC 4211.Contact Information
Instructors
|
Prof. Edmund M. Clarke
emc...@cs.cmu.edu Office: GHC 9231 Phone: (412) 268-2628 Office hours: By appointment |
Dr. Sagar Chaki
cha...@sei.cmu.edu Office: SEI Phone: (412) 268-1436 Office hours: By appointment |
Dr. Arie Gurfinkel
ari...@cmu.edu Office: SEI Phone: (412) 268-7788 Office hours: By appointment |
Teaching Assistants
|
Soonho Kong
cmu1...@gmail.com Office: GHC 7609 Phone: 412-268-3076 Office hours: Monday 16:30 - 17:30 (After Class) |
David Henriques
cmu1...@gmail.com Office: GHC 7511 Phone: 412-268-2582 Office hours: Wednesday 16:30 - 17:30 (After Class) |
Course Secretary
|
Denny Marous
dcm...@cs.cmu.edu Office: GHC 9229 Phone: 412-268-7660 |