Fall 2006 CS750B Software Model Checking

Lecturer

Prof. Moonzoo Kim
Rm# 2434, CS Dept. KAIST
TEL: +82-42-869-3543
mailto:moonzoo [at] cs.kaist.ac.kr

Class and Office Hour

  • Class hour: Tuesday and Thursday 10:30 AM - Noon
  • Office hour: Tuesday and Thursday 1:30 PM - 3:00 PM
  • Classroom: 3444

    Syllubus

  • Background
    As more and more computing systems are deployed as embedded systems in our daily life, the correctness of these systems are becoming crucial issue. Unfortunately, current status of research on formal nature of computing systems is not mature enough for realizing ubiquitous computing without risk. Formal verification can increase the reliability of computing systems with rigorous modeling and complete verification. This class focuses on application of formal verification for software systems.
  • Topics covered during the first half of the class
    First, we will cover model-oriented approach as a starting point. We will handle Calculus of Communicating Systems (CCS) and Promela for this purpose. Process algebra CCS has its advantage in concise syntax and clear semantics and serves as a basic framework of formal verification. In contrast, Promela is a comparatively rich language similar to C. Thus, Promela is more suitable to modeling real systems.
  • Topics covered during the second half of the class
    Then, we will study currently available code-oriented approaches such as BLAST and Java Pathfinder. In these frameworks, a key is how to extract a formal from a complex code through sound abstraction. In addition, we study the Esterel framework which generates C codes from a correctness-proven formal model. Thus, it can serve as a total framework from design to implementation, but with limited expressiveness.

    Administration Policy

  • The official language of this class is English
  • Grade policy:
    Seminar presentations (2 times) 50% (talk should be given in English)
    mid term exam: 30%
    homework (2~3 times): 20%
  • Prerequisite: CS322 Formal language and automata

    Course Schedule

  • Wk 1~3 (Sep 5 ~ Sep 21) : Process algebraic approach - CCS and concurrent workbench
  • Wk 4~6 (Sep 26 ~ Oct 12) : Programming language modeling approach - Promela and SPIN
  • wk 7 (Oct 17 ~ Oct 19): Q&A session and mid-term exam
  • wk 8~13 (Oct 24~ Nov 30): Code-based verification frameworks
  • wk 14~15 (Dec 5 ~ Dec 14): (optional)Esterel - WYPWYE framework (What You Prove is What You Execute)

    Reading Materials

    Main texts of the class are published papers. Realindg list will be announced soon. In addition,
  • Process Algebra by R.Cleaveland and S.A.Smolka
  • The Spin Model Checker 2nd ed by G.Holtzman (Addision-Wesley): Ch2-Ch4, Ch 6
  • The Esterel v5 Language Primer ver. 5.91 by G. Berry (downloadable) Ch2- Ch4
  • Concurrency Workbench of the New Century
    You are required to download and use CWB-NC for HW#1. Also download user's manual for your reference.
  • End-to-End Deployment of Formal Methodology - a Case Study on Multiple Reader/Writer Program by M.Kim and I.Kang
    You are recommended to read this article which explains the detail of class material on Sep 19.
  • The Linear Time-Branching Time Spectrum I by R.J. van Glabbeek
    You are recommended to read this article which explains the detail of class material on Sep 21.
  • Spin Home Page
    You can download spin from this web pages. You need to install additional SW to use Xspin. Also see Jspin for better user interface for beginners.

    The following three projects are the main topic covered by the second half of this class.
  • BLAST: Berkeley Lazy Abstraction Software Verification Tool
  • SLAM Project
  • Java PathFinder

    Lecture Slides

    If you find any typos and bugs in the lecture slides, please write down those faults at BBS.
    I really appreciate your cooperation to improve this class ^_^
  • Sep 5: Background on Formal Methods
  • Sep 7: Introduction to Process Algebra
  • Sep 12: Formal Semantics of CCS
  • Sep 14: Equivalence Semantics of CCS
  • Sep 19: A Case Study of Reader/Writer
  • Sep 21: Equivalence Hierarchy
  • Sep 26: Linear Temporal Logic (slides of this lecture are from "Logic Model Checking" taught by Dr.G.Holzmann at Caltech Spring 2005)
  • Sep 28: Algebra of Communicating Shared Resources
  • Oct 10: The Spin Model Checker: Part I
  • Oct 12: The Spin Model Checker: Part II
  • Oct 17: The Spin Model Checker: Part III
  • Oct 19: A Case Study: High-Availability Protocol
  • Oct 24: NO CLASS
  • Oct 26: MID-TERM WRITTEN EXAM 10:30-noon
  • Nov 1: MID-TERM PRACTICE EXAM 7-10 pm
    Counter Example Analysis
  • Oct 31: Error Explanation and Fault Localization in Testing Isolating Cause-Effect Chains from Computer Programs" A.Zeller ACM FSE 2002 by Yoonra Choi (slides)
  • Nov 2: Error Explanation and Fault Localization in Model Checking "Error explanation with distance metrics" A.Groce, S.Chake, D.Kroening, O.Strichman, IJTTT vol 8#3 by Yoonra Choi (slides)
    BLAST
  • Nov 7: "Lazy Abstraction" T.A.Henzinger et al, POPL 02 by Jinseong Jeon (slides)
  • Nov 9: "Thread-modular Abstraction Refinement" T.A.Henzinger et al, CAV 03 by SeongGun Kim (slides)
  • Nov 14: "Generating Tests from Counterexamples" Dirk B. et al, ICSE '04 by Jinseong Jeon (slides)
  • Nov 16: "Checking Memory Safety with BLAST" D.Beyer, et all, FASE '05 by SeongGun Kim (slides)
    SLAM
  • Nov 21: SLAM overview by Sangwoon Park - "Automatically Validating Temporal Safety Properties of Interface", T.Ball, S.K.Rajamani, POPL 2002 (slides)
  • Nov 23: c2bp (model creation) by Sangwoon Park - "Automatic Predicate Abstraction of C Programs", T.Ball, R.Majumdar, T.Milstein, S.K.Rajamani, PLDI 2001 (slides)
  • Nov 28: bebop (model checking) by Yoonkyung Ahn -"Bebop: A Symbolic Model Checker for Boolean Programs", T.Ball, S.K.Rajamani, SPIN 2000 (slides)
  • Nov 30: newton(model refinement) by Yoonkyung Ahn - "Generating Abstract Explanations of Spurious Counterexamples in C Programs", T.Ball, S.K.Rajamani (slides)
    Java PathFinder
  • Dec 5: "Model Checking Programs", W.Visser, et al, Automated SE journal vol10#2 2003 by Heejin Ahn
  • Dec 7: "Addressing Dynamic Issues of Program Model Checking", F.Lerda and W.Visser, SPIN 2001 by HyunIk Na
  • Dec 12: "Test Input Generation with Java PathFinder", W.Visser, et al, ISSTA 2004 by Heejin Ahn
    Simplify Theorem Prover
  • Dec 14: "Simplify: A Theorem Prover for a Program Checking" D.Detlefs, G.Nelson, J.B. Saxe by Joseph Kwon

    CS750B Noah Bulletin Board

    Question and comments on this class would be discussed in this bulletin board.