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

CS453 Software Verification Techniques, Fall 11

Announcement

  • Class starts on Sep 1st.
  • No class on Sep 15th
  • No class on Oct 11, 13 due to ATVA/EMSOFT conf.
  • Midterm exam: Oct 25 9:00 - 10:30
  • We have a make-up class on Oct 20
  • Quiz on Nov 3rd on automatic invariant generation
  • Deadline for HW#3 was postponed to Nov 8th.
  • No class on Nov 29, Dec 1 due to ISSRE intl. conf.
  • Deadline for HW#4 was postponed to Nov 27th.
  • We have a make-up class from 2-4 p.m. on Dec 7th at 1101 classroom.
  • Deadline for HW#5 was postponed to Dec 8th.
  • Final exam: Dec 20 9:00 - 12:00

 

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)

  • Teaching assistants: Youngjoo Kim

Office: 2438 (located at the east wing)

Phone:042-350-7743

E-mail: jerry88.kim@gmail.com

Office hour: Mon/Fri 14:00~15:30

(reservation e-mail would be preferred)

  • Lecture hours: Tue & Thr 9:00- 10:30 AM
  • Lecture room: 2445
  • 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.
  • Questions and answers can be done through Noah BBS

 

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 1: Introduction

Sep 6: Necessity for systematic & automated testing techniques

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

Sep 15: no class

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

Sep 22: Logic coverage

Sep 27: Logic coverage from source code 

Sep 29: Category partitioning method (blackbox testing technique)

Oct 4:SAT-based bounded software model checking

Oct 6, Oct 18: Model Checking flash memory storage platform software - an industrial case study

Oct 20:Using SAT solver for Sudoku 

Midterm Exam

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

Nov 1: Automatic Invariant Generation Techniques for Testing - Part I (script)

Nov 3: Automatic Invariant Generation Techniques for Testing - Part II

Nov 8: CREST Tutorial, CREST Examples,  CREST internal

Nov 10: Busybox application examples through CREST

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

Nov 17: Examples of First Order Theories, SMTlib tutorial

Nov 22:Equality and Uninterpreted Function

Nov 24:Decision procedures for equality logic 

Dec 6: Linear Temporal Logic

Dec 7-8: Model checker SPIN part I

Dec 13: Model checker SPIN part II

Dec  20: Final exam

 

Homeworks

Document Actions