Personal tools
You are here: Home Courses CS453 Fall 09

CS453 Formal Software Verification Techniques, Fall 09


  • 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.

  • 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

Office: 2434 (located at the east wing)



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)


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.


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

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

Oct 6: Using SAT solver for Sudoku 

Oct 8: Model Checking flash memory storage platform software - an industrial case study

Oct 13, 27: First order theories

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

             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


  • HW1: Due Sep 22
  • HW2:  Due Oct 6th (see gnu gcov)
  • HW3: Due Oct 15th
  • HW4: Due Oct 29th
  • HW5: Due Nov 26th
  • HW6: Due Dec 8th
  • HW7: Due Dec 20th (No late submissions are allowed)
  • Document Actions