Personal tools
You are here: Home › Courses › CS453 Software Verification Techniques, Fall 10

CS453 SW Verification Techniques, Fall 10

Announcement

  • Aug 28: no class on Sep 7, Nov 9, Nov 11.
  • Sep 7: Bulletin board is open.  Questions and comments can be written here and will be answered within 48 hours.

http://noah.kaist.ac.kr/list.jsp?board=1492

  • A homework box is located in C/S building 3rd floor, near the lecture room 3444 (a.k.a lecture room 5).
  • Sep 25: no class on Sep 28.
  • Sep 30: Make-up class on Oct 6 7:00 PM at the same class room.
  • Oct 12: Logic coverage example slide uploaded
  • Oct 19: HW2 deadline is postponed to Oct 21
  • Oct 28: No class on Nov 9 and Nov 11.
  • Nov 2: HW3 is reduced per your request. No random testing neither exhaustive testing.
  • Nov 3: Class on Nov 4 will start 1:30, not 1:00 PM.
  • Nov 29: Make-up class on Dec 1st 7:00 PM, final exam on Dec 16 1:00 PM

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-350-3543

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

Office hour: Tues/Thurs 2:30-3:30 pm 

(reservation e-mail would be preferred)

  • Teaching assistants: Yunho Kim

Office: 2438 (located at the east wing)

E-mail:  kimyunho@kaist.ac.kr

Phone: 042-350-7743

Office hour: Tues 7:00-9:00 pm

(reservation e-mail would be preferred)

  • Lecture hours: Tue & Thr 1:00- 2:30 PM
  • Lecture room:  3444 (a.k.a lecture room 5)
  • Prerequisite: CS204 Discrete mathematics
  • 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.
    • 10% penalty for missing hardcopy or softcopy
  • Note: The official language in the class is English. All students should submit homeworks in English.

Syllubus

This class covers software verification techniques based on formal methods with reagrd to practical applications, not sophiscated theories.  These automated verification 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 tools and learn about their underlying mechanisms to achieve useful verification results for the target software.

Course Material


Course Schedule

Sep 2: Introduction

Sep 9: Necessity for systematic & automated testing techniques

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

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

Sep 30: Logic coverage

Oct 5: Logic coverage from source code 

Oct 6: Category partitioning method (blackbox testing technique)

Oct 7: SAT-based bounded software model checking 1

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

Oct 19:  Basic SAT Techniques

Oct 26: Midterm Exam

Oct  28: Using SAT solver for Sudoku 

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

Nov 4: CREST Tool, CREST Examples 

Nov 16: CREST internal

Nov 18: Busybox application examples through CREST

Nov 23: First order theories (for concolic testing, UML OCL, etc)

Nov 25: Examples of First Order Theories, SMTlib tutorial

Nov 30: Equality and Uninterpreted Function

Dec 1:Decision procedures for equality logic 

Dec 2: Case study: Concolic testing of multisector read on flash memory

Dec 7: Linear Temporal Logic

Dec 9: Model checker SPIN part I

Principles of the Spin Model Checker by M.Ben-Ari published by Springer

Dec 14: Model checker SPIN part II

Dec 16: Final exam

Homeworks

Document Actions