Personal tools
You are here: Home Courses CS492D Automated SW Analysis, Fall 17

CS492D Automated Software Analysis, Fall 17

Announcement

  • The course number of this class has changed from CS453 (until 2016) to CS492
  • The 1st Class starts on Aug 29, not Sep 5
  • No class on Sep 5 and Sep 7 due to Foundation of Software Engineering conference @ Paderborn Germany
  • We will have a make-up class on Sep 18 (Mon) 8:00- 10:30 PM
  • Oct 9: Changed grading guideline: mid-term exam 10%,  final exam 20%
  • Midterm-exam on Oct 17 9:00-11:00 AM at the classroom.

    Administrative Information

    Office: 2434 (located at the east wing)

    Phone:042-350-3543

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

    Office hour: TBD

    (reservation e-mail would be preferred)

    • Teaching assistants: Hyunsu Lim (bookman01@kaist.ac.kr)
      • TA office hour : TBD
    • Lecture hours: Tues/Thur 9:00-10:15 AM  
    • Lecture room: N1  RM#113
    • Prerequisite: experience in C/C++ programming and linux/unix utilities
    • Grading: attendance/class participation/quiz: 20%, HW: 50%, midterm exam: 10%, final exam:20%
      • 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. 
      • 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.
      • All programming HWs you submit must be able to replayed by executing a single script file on a TA's verifier account (i.e., submitted HW should not have  dependency on your home directory, environment, etc.).  Also, the replayed execution must demonstrate the same output to the submitted hardcopy. You will get 10% penalty of the max score otherwise.
        • For your programming HWs, you should not use external libraries which are not available on the verifier machines.  If you really need an external library, you have to ask TAs to install it on the verifier machines.  
      • More than 7 absences of class will get F grade
        • Late attendance shall be considered as 1/3 absence. 
        • Grad students who are occupied by his/her lab activities (e.g., attending conf, etc.) should submit 1 week prior notice.  
        • No excuse for the absence of class including family issues, illness, etc.
    • The official language in the class is English. All students should submit all written documents such as homeworks, project reports, exams, etc. in English; 20% penalty of the max score otherwise.
    • Questions and answers can be done through KLMS 
    • Excerpts from 강의평가
      • "실질적으로 써먹을 수 있는 내용을 많이 배워서 보람찼습니다"
      • "과제가 많이 어려운것 같았다. 과제에 대한 도움을 수업에서 좀 더 주었으면 좋겠다."

    Syllabus

    This class covers automated SW testing/verification techniques to detect SW bugs effectively and efficiently. In particular, this class focuses to teach techniques that automatically generate test cases to achieve high code coverage and, thus, to detect many bugs.

    The class aims to teach practical applications of advanced testing/verification techniques as well as their underlying algorithms.  This class guides students to use various open-source software testing/verification tools through HWs and learn the underlying mechanisms to maximize the performance of automated testing/verification.

    Course Material

    Course Schedule

    Aug 29 : Introduction [pdf]

    Aug 31: Necessity for systematic & automated testing techniques [pdf]

    Sep 12: Overview on testing techniques (including the input partitioning technique) [pdf]

     

    Part I: Program coverage criteria and program analysis 

    Sep 14: Graph coverage [pdf]

    Sep 18, 19: Graph coverage for source code  [pdf]

    Sep 21: gcov tutorial [pdf], CLang tutorial 1/2: Clang AST [pdf]

    Sep 26: Clang tutorial 2/2: a progam analysis tool by using Clang [pdf]

    Sep 28: Logic coverage [pdf]

    Oct  10:  Logic coverage from source code  [pdf]

    Oct  12 : Mutation testing [pdf],  Q&A session

    Oct  17: Mid-term exam  

     

    Part II: Model checking and Test Oracles

    Oct 24, 26, 31: SAT-based bounded software model checking [pdf]

    Nov 2: Software model checking examples [pdf]

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

     

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

    Nov 9 : Automated SW analysis for high reliability: a Concolic testing approach [pdf]

    Nov 14: CREST Tutorial [pdf] (** important **),   CREST Examples [pdf]

    Nov 16: Symbolic environment example [pdf]

    Nov 21: System-level concolic testing: Busybox application examples through CREST-BV [pdf]

    Nov 23: Unit-level concolic testing: Busybox ls example

     

    Part IV: Verification engince - SAT/SMT solver

    Nov 30: First order theoriesSMTlib tutorial,

    Dec 5:Using SAT solver for Sudoku 

    Dec 7: Static analysis: Coverity, Q&A for final exam

    Dec 12: Final exam  

    Homeworks

    • 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 low-middle (#363), 4th floor (in front of room #403), N1
      • Send your soft copy to TA via KLMS  
    • You have to use a linux account on verifier<X>.kaist.ac.kr for programming HWs.   
      • ID: cs492d_(your student #), initial password: (your student #)!!
        • You have to change your password when you log-in first time.
      • Note that your account will be deleted at the end of the semester.  Don't forget to backup your own data 
    • 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 26 (Tues) 23:59
    2. HW#2 (source code branch coverage measuring tool using Clang, 200 points): due Oct 10 (Tues) 23:59
    3. HW#3 (coverage guided testing, 100 points): due Oct 31 (Tues) 23:59
    4. HW#4 (SAT-based bounded model checking C programs using CBMC, 100 points): due Nov  9 (Thur) 23:59
    5. HW#5 (SAT-based bounded model checking C programs using CBMC continued, 100 points): due Nov  16 (Thur) 23:59
    6. HW#6 (Concolic testing of grep): due Nov 28 (Thurs) 23:59
    Document Actions