CS453 Software Verification Techniques, Fall 12
- 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
- Instructor: Moonzoo Kim
Office: 2434 (located at the east wing)
Office hour: Tues 10:30 AM-1:30 PM
(reservation e-mail would be preferred)
- Teaching assistants: Seokhyeon Mun <firstname.lastname@example.org>
- 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
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.
- "Introduction to Software Testing" by P.Ammann and J.Offutt. Cambridge press 2008
- Reading list
- The Model Checker Spin by G.Holzmann
- Logic in Computer Science 2nd ed by M. Huth and M.RyanLyan
- A Tool for Checking ANSI-C Programs
- DART: Directed Automated Random Testing
- Dictionary for testing terms (한글, English)
- Related tool list
Sep 3: Introduction
Sep 17, 19: Logic coverage
Sep 24: Logic coverage from source code
Sep 26: Category partitioning method (blackbox testing technique)
- "A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study," IEEE Transactions on Software Engineering (TSE), vol 37, no 2, pages 146-160, March 2011
- "Formal Verification of a Flash Memory Device Driver- an Experience Report" by M.Kim, Y.Kim, Y.Choi, and H.Kim
Oct 15:Using SAT solver for Sudoku
Oct 22: Software model checking examples
Nov 12:First order theories (for concolic testing, UML OCL, JML, pre/post condition verification, etc)
Nov 21,26: Equality and Uninterpreted Functions
Nov 28, Dec 3: Linear Temporal Logic
Dec 5: Model checker SPIN part I
- Principles of the Spin Model Checker by M.Ben-Ari published by Springer
Dec 10, 12: Model checker SPIN part II
Dec 17: Final exam
- HW1 : due Sep 27 23:59
- HW2 : due Oct 18 23:59
- HW3: due Nov 8:23:59
- HW4: due Nov 26 23:59
- HW5: due Dec 6 23:59
- HW6: due Dec 14 23:59