15–414/614 Bug Catching: Automated Program Verification

15–414/614 Bug Catching: Automated Program Verification

Spring 2014
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 using Interactive Theorem Proving. Using the proof assistant Coq, we will learn to write machine-checkable proofs for non-trivial logical statements about programs. There will be emphasis on both the theoretical basis of the tool, as well as its hands-on use on real examples. This course can be used as one of the Fundamentals of Algorithms requirement.

Announcements

  • 1/13 Welcome to 15–414/614!

Lectures

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

Contact Information

Instructors

Teaching Assistants

  • Qinsi Wang
    Email: 15414sta@gmail.com
    Office: GHC 9015
    Phone: 412–268–7228
    Office hours: Wednesday, 5pm to 6pm

Course Secretary

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