CS492A Automated Software Analysis, Fall 18
Announcement
- The course number of this class has changed from CS453 (until 2016) to CS492
- Sep 27: The documentation page for Clang 4.0.1 API is now available at the HW section.
- Oct 8: Mid-term exam Oct 17 10:30~12:00 AM
- Dec 3: Final exam on Dec 12 9:00- 12:00 AM
Administrative Information
- Instructor: Moonzoo Kim
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), Kunwoo Park (kunwoo1209@kaist.ac.kr)
- TA office hour: TBD
- Lecture hours: Mon/Wed 10:30 - 11:45 AM
- Lecture room: N1 RM#422
- 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 KLMS 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 be replayed by executing a single script file on a TA's verifier 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 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 the 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 homework, 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
- Textbook
- "Introduction to Software Testing" by P.Ammann and J.Offutt. 2nd ed. Cambridge press 2017
- Reading list
- Dictionary for testing terms (한글, English)
- Beautiful Testing: Leading Professionals Reveal How They Improve Software (Theory in Practice) by Tim Riley and Adam Goucher
- 역사속의 소프트웨어 오류 by 김종하
- The Model Checker Spin by G.Holzmann
- Logic in Computer Science 2nd ed by M. Huth and M.RyanLyan
- Related tool list
Course Schedule
Aug 27 : Introduction [pdf]
Aug 29: Necessity for systematic & automated testing techniques [pdf]
Sep 3: Overview of testing techniques (including the input partitioning technique) [pdf]
Part I: Program coverage criteria and program analysis
Sep 5: Graph coverage [pdf]
Sep 10, 12: Graph coverage for source code [pdf]
- Generating CFG using GCC and Graphviz [pdf]
- http://www.webgraphviz.com/
- Cyclometic complexity (또다른 한글문서)
Sep 17: gcov tutorial [pdf], CLang tutorial 1/2: Clang AST [pdf]
Sep 19: Clang tutorial 2/2: a program analysis tool by using Clang [pdf]
Oct 1: Logic coverage [pdf]
Oct 8: Logic coverage from source code [pdf]
Oct 10 : Mutation testing [pdf], Q&A session
- "Design Of Mutant Operators For The C Programming Language" by Agrawal et al
Oct 17: Mid-term exam 10:30~12:00 AM
Part II: Model checking and Test Oracles
Oct 22, 24: SAT-based bounded software model checking [pdf]
- The importance of unwinding loop bound: SAT-based Bounded Software Model Checking for Embedded Software: A Case Study, APSEC 2014 by Kim et al
Oct 29: Software model checking examples [pdf]
Oct 31: Model Checking flash memory storage platform software - an industrial case study
- "A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study," IEEE Transactions on Software Engineering (TSE), vol 37, no 2, pages 146-160, March 2011
- "Formal Verification of a Flash Memory Device Driver- an Experience Report" Spin 2008, by M.Kim, Y.Kim, Y.Choi, and H.Kim
Part III: Concolic testing (a.k.a., dynamic symbolic execution)
Nov 5 : Automated SW analysis for high reliability: a Concolic testing approach [pdf]
Nov 7: CROWN Tutorial [pdf] (** important **)
Nov 12, 14: CROWN Examples [pdf]
Nov 17: System-level concolic testing: Busybox application examples through CROWN [pdf]
Nov 19: Industrial Application of Concolic Testing on Embedded Software: Case Studies [pdf] [ICSE'12 paper]
Nov 21:Unit-level concolic testing: Busybox ls example [pdf], Automated Unit Testing of Large Industrial Embedded Software using Concolic Testing [pdf] [ASE'13 paper]Part IV: Verification engine - SAT/SMT solver
Nov 26 : Using SAT solver for Sudoku [pdf]
- "Sudoku as a SAT problem" by I.Lynce and J.Ouaknine, Intl. Symp. on Artificial Intelligence and Mathematics 2006
- The SuDoku Puzzle as a Satisfiability Problem
Dec 3: First order theories [pdf] , SMTlib tutorial [pdf],
- Examples of First Order Theories [pdf] (for concolic testing, UML OCL, JML, pre/post condition verification, etc)
- Definition of "theory"
- CS402 Intro to Logic (Predicate Calculus - Semantics)
Dec 5: Static Code Analysis Techniques, LLVM IR basics, CLANG vs LLVM
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 located on the 4th floor of N1 (in front of room #403)
- 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: cs492a_(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
- Clang 4.0.1 API documentation: [Link]
- If you have a question on your HW score, you should post your question on KLMS first.
- HW#1 (structural and dataflow coverage, 100 points) [pdf]: due Sep 19 (Wed) 23:59
- HW#2 (source code branch coverage measuring tool using Clang, 200 points): due Oct 3 (Wed) 23:59
- HW#3 (coverage guided testing, 100 points): due Oct 24 (Wed) 23:59
- HW#4 (SAT-based bounded model checking C programs using CBMC, 100 points): due Nov 7 (Wed) 23:59
- HW#5 (SAT-based bounded model checking C programs using CBMC continued, 100 points): due Nov 14 (Wed) 23:59
- HW#6 (Concolic testing, 100 points): due Nov 19 (Mon) 23:59
- HW#7 (Concolic testing of grep, 100 pts): due Nov 28 (Wed) 23:59
- HW#8 (concolic UNIT testing on regex_compile() on grep, 200 points): due Dec 3 (Mon) 23:59
- grep-v2.0-code
- code review slide for regex_compile function (Eng)
- code review slide for regex_compile function (Kor)
- HW#9 (SMT solver, 100 points) [pdf]: due Dec 10 (Mon) 23:59