Announcement
- Aug 30: no class on Sep 1st
- 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=1408
- A homework box is located in C/S building 2nd floor, near the lecture room 2444 (a.k.a lecture room 3).
- Sep 22: We will have a quiz on Sep 24th
- Sep 23: "MODEL-driven test design: tutorial" by Prof. J.Offutt (the author of "Intro. to SW Testing") @ sogang univ, Oct 14
- Mid-term exam on Oct 22nd 10:30-12:00 AM (CLOSED BOOK)
- No class on Nov 3 and Nov 5 due to FM 2007 intl. conf.
- Problem 2-2 in HW6 is removed. You do not need to modify flash_read() function.
- Visit TA's office(CS Bldg. #2438) and bring back your homeworks during 14th, December(Monday) 1pm to 3pm, and 7pm to 10pm
- Finam exam on Dec 15 10:30-12:00 AM (CLOSED BOOK)
- Bring back your final exam answer sheets and and HW7 until this Tuesday(29th Dec.).
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 4:30-6: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-3583
Office hour: Tues 7:00-9:00 pm
(reservation e-mail would be preferred)
- Lecture hours: Tue & Thr 10:30 - 12:00
- Lecture room: 2444 (a.k.a lecture room 3)
- Prerequisite: CS204 Discrete mathematics
-
Grading: attendance and quiz: 20%, HW: 50%, midterm exam: 15%, final exam:15%
- Late HW is accepted with 20% penalty in 1 day, 40% 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
- "Decision procedures - an algorithmic approach" by D.Kroening and O.Strichman
- "The calculus of computation" by A.R.Bradley and Z.Manna, Springer 2007
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
Related tool list
Course Schedule
- Sep 3: Introduction
- Sep 8: Necessity for systematic & automated testing techniques
- Sep 10: Graph coverage (see Intro to Software Testing web sige)
- Sep 15: Graph coverage for source code (see Understand C++)
- Sep 17: Logic coverage
- Sep 22: Logic coverage from source code
- Sep 24: SAT-based bounded software model checking 1
- Sep 29: Basic SAT Techniques
- "The quest for efficient Boolean satisfiability solvers" by L.Zhang and S.Malik, CAV 2002
- Oct 6: 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
- Oct 8: 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 13, 27: First order theories
- Definition of "theory"
- CS402 Intro to Logic (Predicate Calculus - Semantics)
- Oct 29: Examples of first order theories
- Nov 10: Equalities and uninterpreted functions
- Nov 12: Decision procedures for equality logic - Intro
- Nov 17: Transforming decision procedure for equality to propositional logic
- Nov 18: SMT-LIB: The Satisfiability Modulo Theories Library
- Nov 19: "CUTE: A Concolic Unit Testing Engine for C" by K.Sen, et al. FSE 05
- Nov 24: CREST Tutorial (a technical report on CREST)
- Nov 26: Verification by Contract: WHY tool
- Dec 1: Counter-example guided abstraction refinement (CEGAR) - BLAST
- ("The Software Model Checker Blast: Applications to Software Engineering" by Dirk Beyer et. al in Int. Journal on Software Tools for Technology Transfer, 2007)
- Dec 3: Linear Temporal Logic
- Dec 8: Model checker SPIN part I
- Principles of the Spin Model Checker by M.Ben-Ari published by Springer
- Dec 10: Model checker SPIN part II