CS453 Formal Software Verification Techniques, Fall 09

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.

Syllubus

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
• Spin home page
• CBMC home page 
• MiniSAT home page
• Yices home page
• Z3 home page
• CREST home page
• WHY home page

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

• Ch 3 of "The calculus of computation"

Nov 10: Equalities and uninterpreted functions

Nov 12: Decision procedures for equality logic - Intro

Nov 17: Transforming decision procedure for equality to propositional logic

             Combination of theories

Nov 18: SMT-LIB: The Satisfiability Modulo Theories Library

              SMTLIB tutorial

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)

             Concolic testing of flash memory storage platform software - an industrial case study (SBMF 09 paper)

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

Homeworks