Announcement
- Class starts on Sep 1st.
- No class on Sep 15th
- No class on Oct 11, 13 due to ATVA/EMSOFT conf.
- Midterm exam: Oct 25 9:00 - 10:30
- We have a make-up class on Oct 20
- Quiz on Nov 3rd on automatic invariant generation
- Deadline for HW#3 was postponed to Nov 8th.
- No class on Nov 29, Dec 1 due to ISSRE intl. conf.
- Deadline for HW#4 was postponed to Nov 27th.
- We have a make-up class from 2-4 p.m. on Dec 7th at 1101 classroom.
- Deadline for HW#5 was postponed to Dec 8th.
- Final exam: Dec 20 9:00 - 12:00
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: Youngjoo Kim
Office: 2438 (located at the east wing)
Phone: 042-350-7743
E-mail: jerry88.kim@gmail.com
Office hour: Mon/Fri 14:00~15:30
(reservation e-mail would be preferred)
- Lecture hours: Tue & Thr 9:00- 10:30 AM
- Lecture room: 2445
- 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.
- Questions and answers can be done through Noah BBS
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 1: Introduction
- Sep 6: Necessity for systematic & automated testing techniques
- Sep 8: Graph coverage (see Intro to Software Testing web sige)
- Sep 15: no class
- Sep 20: Graph coverage for source code (see Understand C++)
- Sep 22: Logic coverage
- Sep 27: Logic coverage from source code
- Sep 29: Category partitioning method (blackbox testing technique)
- Oct 4: SAT-based bounded software model checking
- Oct 6, Oct 18: Model Checking flash memory storage platform software - an industrial case study
- "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 20: 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
- Midterm Exam
- Oct 27: Automated SW analysis for high reliability: a Concolic testing approach
- Nov 1: Automatic Invariant Generation Techniques for Testing - Part I (script)
- Nov 3: Automatic Invariant Generation Techniques for Testing - Part II
- Nov 8: CREST Tutorial, CREST Examples, CREST internal
- Nov 10: Busybox application examples through CREST
- Nov 15: First order theories (for concolic testing, UML OCL, JML, pre/post condition verification, etc)
- Definition of "theory"
- CS402 Intro to Logic (Predicate Calculus - Semantics)
- Nov 17: Examples of First Order Theories, SMTlib tutorial
- Nov 22: Equality and Uninterpreted Function
- Nov 24: Decision procedures for equality logic
- Dec 6: Linear Temporal Logic
- Dec 7-8: Model checker SPIN part I
- Principles of the Spin Model Checker by M.Ben-Ari published by Springer
- Dec 13: Model checker SPIN part II
- Dec 20: Final exam