Announcement
- Aug 28: no class on Sep 7, Nov 9, Nov 11.
- Sep 7: Bulletin board is open. Questions and comments can be written here and will be answered within 48 hours.
- http://noah.kaist.ac.kr/list.jsp?board=1492
- A homework box is located in C/S building 3rd floor, near the lecture room 3444 (a.k.a lecture room 5).
- Sep 25: no class on Sep 28.
- Sep 30: Make-up class on Oct 6 7:00 PM at the same class room.
- Oct 12: Logic coverage example slide uploaded
- Oct 19: HW2 deadline is postponed to Oct 21
- Oct 28: No class on Nov 9 and Nov 11.
- Nov 2: HW3 is reduced per your request. No random testing neither exhaustive testing.
- Nov 3: Class on Nov 4 will start 1:30, not 1:00 PM.
- Nov 29: Make-up class on Dec 1st 7:00 PM, final exam on Dec 16 1:00 PM
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/Thurs 2:30-3:30 pm
(reservation e-mail would be preferred) -
Teaching assistants: Yunho Kim
Office: 2438 (located at the east wing)
E-mail: kimyunho@kaist.ac.kr
Phone: 042-350-7743
Office hour: Tues 7:00-9:00 pm
(reservation e-mail would be preferred)
- Lecture hours: Tue & Thr 1:00- 2:30 PM
- Lecture room: 3444 (a.k.a lecture room 5)
- Prerequisite: CS204 Discrete mathematics
-
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.
- 10% penalty for missing hardcopy or softcopy
- Note: The official language in the class is English. All students should submit homeworks in English.
Syllabus
This class covers software verification techniques based on formal methods with reagrd to practical applications, not sophiscated theories. These automated verification 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 tools and learn about their underlying mechanisms to achieve useful verification results for the target software.
Course Material
Textbook
- "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
Course Schedule
- Sep 2: Introduction
- Sep 9: Necessity for systematic & automated testing techniques
- Sep 14: Graph coverage (see Intro to Software Testing web sige)
- Sep 16: Graph coverage for source code (see Understand C++)
- Sep 30: Logic coverage
- Oct 5: Logic coverage from source code
- Oct 6: Category partitioning method (blackbox testing technique)
- Oct 7: SAT-based bounded software model checking 1
- Oct 14: Model Checking flash memory storage platform software - an industrial case study
- "Unit Testing of Flash Memory Device Driver through a SAT-based Model Checker" by M.Kim, Y.Kim and H.Kim
- "Formal Verification of a Flash Memory Device Driver- an Experience Report" by M.Kim, Y.Kim, Y.Choi, and H.Kim
- Oct 19: Basic SAT Techniques
- "The quest for efficient Boolean satisfiability solvers" by L.Zhang and S.Malik, CAV 2002
- Oct 26: Midterm Exam
- Oct 28: Using SAT solver for Sudoku
- "Sudoku as a SAT problem" by I.Lynce and J.Ouaknine, Intl. Symp. on Artificial Intelligence and Mathematics 2006
- The SuDoku Puzzle as a Satisfiability Problem
- Nov 2: Automated SW analysis for high reliability: a Concolic testing approach
- Nov 4: CREST Tool, CREST Examples
- Nov 16: CREST internal
- Nov 18: Busybox application examples through CREST
- Nov 23: First order theories (for concolic testing, UML OCL, etc)
- Definition of "theory"
- CS402 Intro to Logic (Predicate Calculus - Semantics)
- Nov 25: Examples of First Order Theories, SMTlib tutorial
- Nov 30: Equality and Uninterpreted Function
- Dec 1: Decision procedures for equality logic
- Dec 2: Case study: Concolic testing of multisector read on flash memory
- Dec 7: Linear Temporal Logic
- Dec 9: Model checker SPIN part I
- Principles of the Spin Model Checker by M.Ben-Ari published by Springer
- Dec 14: Model checker SPIN part II
- Dec 16: Final exam
Homeworks
- HW1: Due Sep 28 23:59
- HW2: Due Oct 21 23:59
- A step-by-step instruction on how to build busybox with gcov and get coveratge information
- (reduced) HW3: Due Nov 9 23:59
- HW4: Due Nov 30 23:59
- HW5: Due Dec 14 23:59
- (Extra Credit) HW: Due Dec 21 23:59 (no late hw accepted)