CS492 Automated Software Analysis, Fall 17
- No class on Nov 23 due to interview of undergraduate applicants
- HW#4 was revised, and now you are allowed to generate more than 1,000 test cases per each strategy.
- Explanation slide for regex_compile() was uploaded.
(The slide is written in Korean. The English version will be uploaded by this afternoon(Nov 24).
- If you like the material of CS492 or automated testing, please apply for URP or independence study with me :-)
- Instructor: Moonzoo Kim
Office: 2434 (located at the east wing)
Office hour: TBD
(reservation e-mail would be preferred)
- Teaching assistants: Hyunwoo Kim (email@example.com, x7743), Woong-Gyu Yang(firstname.lastname@example.org, x7747)
- TA office hour : Mon 2:30-4:00 PM / Wed 6:30-8:00 PM (Room #403, N-1)
- Lecture hours: Mon/Wed 1-2:15 PM
- Lecture room: 422 (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.
- 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 강의평가
- "실질적으로 써먹을 수 있는 내용을 많이 배워서 보람찼습니다"
- "과제가 많이 어려운것 같았다. 과제에 대한 도움을 수업에서 좀 더 주었으면 좋겠다."
This class covers automated software verification/testing techniques to fight the high complexity of software. 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 guides students to utilize various software verification/testing tools and learn the underlying mechanisms to produce verification results for the target software effectively and efficiently.
- "Introduction to Software Testing" by P.Ammann and J.Offutt. Cambridge press 2008
- Reading list
- The Model Checker Spin by G.Holzmann
- Logic in Computer Science 2nd ed by M. Huth and M.RyanLyan
- A Tool for Checking ANSI-C Programs
- DART: Directed Automated Random Testing
- Dictionary for testing terms (한글, English)
- Related tool list
Sep 5 : Introduction
Sep 12 night: Overview on testing techniques (including the input partitioning technique)
Part I: Program coverage criteria and program analysis
Sep 19,21: Graph coverage
Sep 26: Graph coverage for source code
Oct 10: Logic coverage
Oct 12: Logic coverage from source code
Part II: Concolic testing (a.k.a., dynamic symbolic execution)
Oct 19 : Q&A session
Oct 24: Mid-term exam
Oct 31: CREST Tutorial (** important **)
Nov 2: CREST Examples
Nov 7: Symbolic environment example
Nov 9: System-level concolic testing: Busybox application examples through CREST-BV
Nov 14: Unit-level concolic testing: Busybox ls example
Part III: Model checking
Nov 21, 28: SAT-based bounded software model checking
- The importance of unwinding loop bound: SAT-based Bounded Software Model Checking for Embedded Software: A Case Study, APSEC 2014 by Kim et al
- "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 IV: Verification engince - SMT/SAT solver
- Examples of First Order Theories(for concolic testing, UML OCL, JML, pre/post condition verification, etc)
Dec 12 :Using SAT solver for Sudoku
- "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 14: Static analysis: Coverity, Q&A for final exam
Dec 19: Final exam (1:00-3:00 PM)
- 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 (in front of room #403), N1
- Email address for a soft copy: send your soft copy to both 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>.kaist.ac.kr for programming HWs.
- ID: cs453_(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.
- HW#1 (structural and dataflow coverage, 100 points): due Oct 3 (Mon) 23:59, submit your HW to Hyunwoo TA
- HW#2 (source code branch coverage measuring tool using Clang, 200 points): due Oct 17 (Mon) 23:59
- HW#3 (concolic testing on grep, 200 points): due Nov 14 (Mon) 23:59
- HW#4 (concolic UNIT testing on regex_compile() on grep, 200 points): due Nov 28 (Mon) 23:59
- code review slide for regex_compile function (Kor)
- code review slide for regex_compile function (Eng)
- HW#5 (SAT-based bounded model checking C programs using CBMC, 100 points): due Dec 7 (Wed) 23:59
- HW#6 (Model checking with SMT solver, 100 points): due Dec 16 (Fri) 23:59