CS453 Software Verification Techniques, Fall 12

Announcement

  • Aug 30: Class starts on Sep 1st
  • Oct 8: Mid term exam on Oct 22 (Mon) 12:30 - 1:00 PM at the classroom.
  • Oct 10: Mid term exam time is changed to Oct 29 (Mon) 12:30 - 2:00 PM at the classroom.
  • Oct 22: Slides of software model checking examples are uploaded.
  • Nov 12: No class on Nov 14 due to FSE intl. conf.
  • Nov 19: For HW#4, please send your information (student id, full name, and desired user id) to TA by tonight. We will provide you a temporary user account where you can do HW#4.
    • Note that the user account will be deleted on Nov 30.
  • Nov 20: Your account for HW# 4 is created. You can access the machine (URL: tester2.kaist.ac.kr) by using your desired ID and Password which is your student number.
    • Only 5 students requested accounts. If you want to use tester2, send mail to TA by tonight.
  • Dec 3: Final exam on Dec 17(Mon) 12:30-2:30 PM
  • Dec 12: Final exam scope will include CBMC model checking, too

Administrative Information

  • Instructor: Moonzoo Kim

    Office: 2434 (located at the east wing)
    Phone: 042-350-3543
    E-mail: moonzoo@cs.kaist.ac.kr
    Office hour: Tues 10:30 AM-1:30 PM
    (reservation e-mail would be preferred)

  • Teaching assistants: Seokhyeon Mun <seokhyeon.mun@gmail.com>
  • Lecture hours: Mon & Wed 12:30 - 1:45 PM
  • Lecture room: 2445
  • Prerequisite: experience in C programming
  • Grading: attendance and quiz: 20%, HW: 50%, midterm exam: 15%, final exam:15%
    • Late HW is accepted with 10% penalty in 1 day, 30% penalty in 3 days. HW will not be accepted after then.
    • HW should be submitted both in hardcopy and softcopy (through email to TA). 10% penalty for missing hardcopy or softcopy.
  • Note: The official language in the class is English. All students should submit homeworks in English.
  • Questions and answers can be done through Noah BBS

Syllabus

This class covers automated software verification/testing techniques. The goal of the class is to learn practical applications of advanced verification/testing techniques, not sophiscated theories. These automated techniques can provide high reliability for complex embedded software compared to traditional testing methods in a more productive way. This class utilizes various software verification/testing tools and learns their underlying mechanisms to produce verification results for the target software.

Course Material

Course Schedule

Homeworks