Personal tools
You are here: Home › Courses › CS458 Dynamic Analysis of Software Source Code, Fall 22

CS458 Dynamic Analysis of Software Source Code, Fall 22

Announcement

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-350-3543

E-mail: moonzoo.kim @ gmail.com

Office hour: Tues 4:00-5:00 PM

(reservation e-mail is preferred)

  • Teaching assistants: Ahcheong Lee (ahcheong.lee@gmail.com)
  • Lecture hours: Tue/Thur 2:30 - 3:45 PM
  • Lecture room: E3 Rm#2111 (and through Zoom)
    • I plan to make a face-to-face lecture on Tues and an online lecture on Thurs
      • the plan may change later depending on the academic performance of the class participants.
    • Zoom link for Thurs class: https://kaist.zoom.us/j/5258253316
  • Prerequisite: proficiency in C/C++ programming and Linux utilities
    • Due to the high load of TA, TA will not provide help for basic C/C++/Linux questions.
    • Highly recommend to take CS458 after taking CS230 System Programming first
  • Grading: attendance/class participation/quiz: 25%, HW: 50%, final exam:25%
    • You should turn on your web cam when you participate an online class; class attendance will not be counted otherwise.
    • 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.
      • Hint: many questions of exams are from the homework.
    • All programming HWs you submit must be able to be replayed by executing a single script file on a TA's server account (i.e., submitted HW should not have a dependency on your home directory, environment, etc.).  Also, the replayed execution must demonstrate the same output to the submitted hw. 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 server machines.  If you really need an external library, you have to ask TAs to install it on the server machines.
    • More than 7 absences of the class will get F grade
      • Late attendance shall be counted as 1/3 absence.
      • If a student is not able to attend a class due to an important event (e.g., attending conf., etc.), he/she should submit 1 week prior notice to the professor.
  • The official language in the class is English. All students should submit all written documents such as homework, project reports, exam, 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

Part I: Overview of software complexity and testing

“Software testers do not make software; they only make them better.” – Anonymous

Aug 30 : Introduction [pdf]

Sep 1: Necessity for systematic & automated testing techniques [pdf]

Sep 6: Overview of testing techniques (including the input partitioning technique) [pdf]

 

Part II: Source code coverage criteria for effective SW debugging

“It’s hard enough to find an error in your code when you’re looking for it; it’s even harder when you’ve assumed your code is error-free.”— Steve McConnell

Sep 8, 13: Graph coverage [pdf]

Sep 15: Graph coverage for source code [pdf]

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

Sep 22: Clang tutorial 2/2: a program analysis tool by using Clang [pdf]

Sep 27: Logic coverage [pdf]

Sep 29:  Logic coverage from source code [pdf]

Oct  4: No class (requested by KAIST)

Oct  6 : Mutation testing [pdf],  Q&A session for coverage guided whitebox testing

 

Part III: Model checking and test oracles

Oct 11, 13: SAT-based bounded software model checking [pdf]

Oct 18, 20: No class due to midterm exam

Oct 25, 27: Software model checking examples [pdf]

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

Nov 3: Verification of the multi-sector read of flash memory storage

 

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

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

Nov 10: no class

Nov 15: no class

Nov 17: CROWN Tutorial

Nov 22, 24: CROWN Examples, compared to CBMC Memory Model, application of concolic testing to the circular queue example

Nov 29: System-level concolic testing: Busybox application examples through CROWN

Dec 1 (Makeup class 1): Automated unit testing, Unit-level concolic testing: Busybox ls example

Online makeup class 2 (pre-recorded movie clip):


Part V: Verification engine - SAT/SMT solver

Dec 6: SMTlib tutorial, SMTlib web page, First order theories [pdf]

Dec 8: Using SAT solver for Sudoku, Q&A for the final exam, LLVM IR basics, CLANG vs LLVM

Dec 15 (13:00~15:30): Final exam (closed book)

 

Homeworks

Document Actions