Personal tools
You are here: Home › Courses › CS453 SW Verification. Tech., Fall 12

CS453 Software Verification Techniques, Fall 12

Announcement

  • Aug 30: Class starts on Sep 1st
  • Oct 8: Mid term exam on Oct 22 (Mon) 12:30 - 1:00 PM at the classroom.
  • Oct 10: Mid term exam time is changed to Oct 29 (Mon) 12:30 - 2:00 PM at the classroom.
  • Oct 22: Slides of software model checking examples are uploaded.
  • Nov 12: No class on Nov 14 due to FSE intl. conf.
  • Nov 19: For HW#4, please send your information (student id, full name, and desired user id) to TA by tonight. We will provide you a temporary user account where you can do HW#4.
    • Note that the user account will be deleted on Nov 30.
  • Nov 20: Your account for HW# 4 is created. You can access the machine (URL: tester2.kaist.ac.kr) by using your desired ID and Password which is your student number.
    • Only 5 students requested accounts. If you want to use tester2, send mail to TA by tonight.
  • Dec 3: Final exam on Dec 17(Mon) 12:30-2:30 PM
  • Dec 12: Final exam scope will include CBMC model checking, too

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-350-3543

E-mail: moonzoo@cs.kaist.ac.kr

Office hour: Tues 10:30 AM-1:30 PM

(reservation e-mail would be preferred)

  • Lecture hours: Mon & Wed 12:30 - 1:45 PM
  • Lecture room: 2445
  • Prerequisite: experience in C programming
  • Grading: attendance and quiz: 20%, HW: 50%, midterm exam: 15%, final exam:15%
    • Late HW is accepted with 10% penalty in 1 day, 30% penalty 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.
  • Note: The official language in the class is English. All students should submit homeworks in English.
  • Questions and answers can be done through Noah BBS

  

 

Syllubus

 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

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

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

Sep 17, 19: Logic coverage

Sep 24: Logic coverage from source code 

Sep 26: Category partitioning method (blackbox testing technique)

Oct 8:SAT-based bounded software model checking

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

Oct 15:Using SAT solver for Sudoku 

Oct 22: Software model checking examples

Midterm Exam

Oct 31: Automated SW analysis for high reliability: a Concolic testing approach

Nov 5: CREST Tutorial, CREST Examples,  CREST internal

Nov 7: Busybox application examples through CREST

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

Nov 19: Examples of First Order Theories, SMTlib tutorial,

Nov 21,26: Equality and Uninterpreted Functions

Nov 28, Dec 3: Linear Temporal Logic

Dec 5: Model checker SPIN part I

Dec 10, 12: Model checker SPIN part II

Dec 17: Final exam

  

Homeworks

Document Actions