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

CS453 Automated Software Testing, Fall 13


  • Sep 14: No class on Sep 17. Happy Chuseok!
  • Sep 26: A report box for homwork is created at box #392, 4th floor, N1 building 
  • Oct 1: HW2 is released. I prepared linux machines for your programming homework. Please see Noah BBS.
  • Oct 15: Midterm exam on Oct 31 (Thurs) 9:00 - 10:15 AM
  • Oct 15: No class on Nov 5th (Tues) due to visiting HKUST for CS dept. seminar.
  • Oct 15: We will have make-up classes on Oct 24 at regular class time.
  • Dec 16: Final exam on Dec 17 (Tue) 9:00 AM - 12:00 PM

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: 박용배 (Yongbae Park)  yongbae2 @ g m a i l . c o m
  • Lecture hours: Tues & Thurs 9:00 - 10:15 AM
  • Lecture room: 113 (N-1)
  • Prerequisite: experience in C/C++ programming and linux/unix command-line utilities.
  • Grading: attendance/class participation/quiz: 20%, HW: 50%, midterm exam: 15%, final exam:15%
    • Late HW is 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.
    • HW should be submitted both in hardcopy and softcopy (through email to TA). 10% penalty for missing hardcopy or softcopy.
    • More than 8 absences of class will get F grade
      • To start class on time, late attendance is considered as 1/3 absence. 
    • Hint: many questions of exams are from the homework.
  • Note: 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 sophiscated 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 3 : Introduction

Sep 5: Necessity for systematic & automated testing techniques

Part I: Coverage criteria

Sep 10: Graph coverage (see Intro to Software Testing web sige)

Sep 12,24: Graph coverage for source code (see Understand C++ )

Sep 26: Logic coverage

Oct 1: CLang tutorial to build a branch coverage measuring tool 

Oct 8: Logic coverage from source code 

Oct 10: Category partitioning method (blackbox testing technique)

Part II: Software model checking

Oct 15,17:SAT-based bounded software model checking

Oct 22: Software model checking examples

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

Oct 29:SAT solver heuristicsUsing SAT solver for Sudoku 

Oct 31: Midterm Exam

Part III: Logic model checking

Nov 7:  Model checker SPIN part I

Nov 12: Model checker SPIN part II

Nov 19:Linear Temporal Logic

Part IV: Concolic testing

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

Nov 26: CREST Tutorial 

Nov 28: CREST ExamplesBusybox application examples through CREST-BV 

Dec 3: Industrial Application of Concolic Testing on Embedded Software: Case Studies [ICSE'12 paper]

Dec 5: Automated Unit Testing of Large Industrial Embedded Software using Concolic Testing  [ASE'13 paper] 

Dec 10 :First order theories (for concolic testing, UML OCL, JML, pre/post condition verification, etc)

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

Dec 17: Final exam



  • You need to submit both a hard copy and a soft copy for each homework.
    • Report box for a hard copy: report box #392, 4th floor, N1 building 
    • Email address for a soft copy: send your soft copy to TA ( via email.
      • Please put [CS453] at the beginning of the title (ex. [CS453] Homework #1)


  • HW1 : due Oct 1st 23:59
  • HW2: due Oct 10 23:59
  • HW3: due Oct 22 23:59
  • HW#4: due Oct 31 23:59
  • HW#5: due Nov 17 23:59 (due date is postponed)
  • HW#6: due Nov 26 23:59
  • HW#7: due Dec 6 23:59
    • Martin Heisterman achieved the highest gcov branch coverage (53.69%) in HW7.
  • HW#8: due Dec 17 23:59
  • Extra HW (optional 300 pts, delayed HW will not be accepted): due Dec 24 23:59
    • Do the HW#7 question 2 with the goal to improve the gcov branch coverage of grep.c higher than 60%
      • You should provide all answers for the 5 sub-questions
      • If you achieve higher than 50% of the gcov branch coverage, you can get 200 pts
        • If you already achieve more than 50%, just send an e-mail to TA to get 200 pts free.
      • If you achieve higher than 40% of the gcov branch coverage, you can get 100 pts
        • If you already achieve more than 40%, just send an e-mail to TA to get 100 pts free.
Document Actions