Personal tools
You are here: Home Courses CS453 Automated SW Testing, Fall 14

CS453 Automated Software Testing, Fall 14


  1. Final term exam on Dec 16 (Tues) 9:00-11:00 AM at N1 RM# 114
  2. HW#6 deadline is postponed to Dec 5 (Friday)
  3. Another make-up class 8:00-10:30 PM Dec 8th (Monday)
  4. Make-up class 9:00-11:30 PM  Nov 25 (Tuesday)
  5. We will have a global lecture series on model checking and symbolic execution by Prof. Willem Visser (a  pioneer of software model checking techniques). I highly recommend you to attend the class.
    • Time: Nov 24 (Mon) to 28 (Fri) 2:00 PM - 5:00 PM 
    • Place: Osangsu seminar room @ the 4th floor of E3-1.  
  6. No class on Nov 18, 20 due to FSE.
  7. Mid term exam on Oct 21 9:00-11:00 AM at N1 RM# 114

Administrative Information

Office: 2434 (located at the east wing)


E-mail: moonzoo @ c s . k a i s t . a c . k r

Office hour: Tues 10:30 AM-1:30 PM

(reservation e-mail would be preferred)

  • Teaching assistants: Shin Hong ( and Taehoon Kwak (
  • Lecture hours: Tues & Thurs 9:00 - 10:15 AM
  • Lecture room: 114 (N-1)
  • Prerequisite: experience in C/C++/Java programming and linux/unix command-line utilities.
  • Grading: attendance/class participation/quiz: 20%, HW: 50%, midterm exam: 15%, final exam:15%
    • Late HW will be accepted with 10% penalty of the max score in 1 day, 30% penalty of the max score in 3 days. HW will not be accepted after then (i.e., HW that passes the hard deadline).
    • HW should be submitted both in hardcopy and softcopy (through email to TA). 10% penalty of the max score for missing hardcopy or softcopy unless explicitly written in HW. 
      • Hint: many questions of exams are from the homework.
    • More than 8 absences of class will get F grade
      • To start early morning class on time, late attendance shall be considered as 1/3 absence. 
  • The official language in the class is English. All students should submit homeworks in English; 10% penalty otherwise
  • Questions and answers can be done through Noah BBS
  • Excerpts from 강의평가
    • "실질적으로 써먹을 수 있는 내용을 많이 배워서 보람찼습니다"
    • "과제가 많이 어려운것 같았다. 과제에 대한 도움을 수업에서 좀 더 주었으면 좋겠다."


 This class covers automated software verification/testing techniques. The goal of the class is to learn practical applications of advanced verification/testing techniques, not sophisticated theories.  These automated 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/testing tools and learns their underlying mechanisms to produce verification results for the target software.

Course Material

Course Schedule

Sep 2 : Introduction

Sep 4: Necessity for systematic & automated testing techniques

Part I: Program coverage criteria and program analysis tools

Sep 11, 16: Graph coverage 

Sep 18: Graph coverage for source code 

Sep 23: gcov tutorial, CLang tutorial 1/2: Clang AST

Sep 25: Clang tutorial 2/2: a progam analysis tool by using Clang

Sep 30, Oct 2: Logic coverage

Oct 7:  Logic coverage from source code 

Oct 14: LLVM IR tutorial 1/2

Oct 16: LLVM IR tutorial 2/2

Oct 21: Mid-term exam


Part II: Model checking

Oct 28:SAT-based bounded software model checking

Oct 30: Software model checking examples

Nov  4: Model Checking flash memory storage platform software - an industrial case study

Nov 6:Using SAT solver for Sudoku, SAT solver heuristics

Nov 11:  Model checker SPIN part I

Nov 13: Model checker SPIN part II

Nov 25, 27:Linear Temporal Logic


Part III: Concolic testing (a.k.a., dynamic symbolic execution)

Nov 27: Automated SW analysis for high reliability: a Concolic testing approach

Dec 2: CREST Tutorial

Dec 8: CREST ExamplesBusybox application examples through CREST-BV 

Dec 11: Examples of First Order Theories, SMTlib tutorial,

Dec 16: Final exam


  • You need to submit both a hard copy and a soft copy for each homework.
    • Report box for a hard copy: the report box of top-left corner (#385), 4th floor, N-1
    • Email address for a soft copy: send your soft copy to TAs via email (
      • Please put [CS453] at the beginning of the title (ex. [CS453] Homework #1)
  • You have to use a linux account on verifier<X> for HW.  See the class noah bbs for detail
  • We will try to give you feedback on your homework in 1 week from the hard deadline.
  • If you have a question on your HW score, you should contact TA first.
    1. HW#1 (structural and dataflow coverage, 100 points): due Sep 25 (Thurs) 23:59
    2. HW#2 (coverage testing, 100 points): due Sep 30 (Tues) 23:59
      3.  HW#3 (source code branch coverage measuring tool using Clang, 200 points): due Oct 9 (Thurs) 23:59
      5. HW#5 (SAT-based bounded model checking C programs using CBMC): due Nov 13 (Thurs) 23:59
      6. HW# 6 (Model checking using Spin): due Dec 5 (Friday) 23:59
      7. HW#7 (Concolic testing): due Dec 24 (Wed) 23:59
    Document Actions