15–414/614 Bug Catching: Automated Program Verification

15–414/614 Bug Catching: Automated Program Verification

Fall 2012 Semester
Computer 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 two important and alternative approaches – Interactive Theorem Proving and Model Checking. Using the proof assistant Coq, we will learn to write machine-checkable proofs for non-trivial logical statements about programs. The ideas we discuss in Model Checking include propositional satisfiability, Binary Decision Diagrams, temporal-logic model checking, abstraction, abstraction-refinement, bounded model checking and compositional reasoning. 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

  • 8/27 Welcome to 15–414/614!

Lectures

Monday and Wednesday from 3:00 to 4:20 pm in GHC 4102.

Contact Information

Instructors

Teaching Assistants

  • Anvesh Komuravelli
    cmu1…@gmail.com
    Office: GHC 7503
    Phone: 412–268–5143
    Office hours: Tuesday, 4 pm to 5 pm
  • Qinsi Wang
    cmu1…@gmail.com
    Office: GHC 7517
    Phone: 412–268–7228
    Office hours: Thursday, 5 pm to 6 pm

Course Secretary

  • Charlotte Yano
    yan…@cs.cmu.edu
    Office: GHC 9229
    Phone: 412–268–7656