CS750B Special Topic : Formal Verification, Fall 06

Administrative Information

Instructor : Moonzoo Kim

  • Office: 2434 (located at the east wing)
  • Phone: 042-869-3543
  • E-mail: moonzoo@cs.kaist.ac.kr
  • Lecture hour : Tuesday and Thursday 10:30 AM - Noon
  • Office hour : Tuesday and Thursday 1:30 PM - 3:00 PM
  • Classroom : 3444
  • Grade policy:
    • Seminar presentations (2 times) 50% (talk should be given in English)
    • Midterm exam : 30%
    • Homework (2~3 times) : 20%
  • Prerequisite: CS322 Formal language and automata
  • Note: The official language of this class is English

Syllabus

Background

As more and more computing systems are deployed as embedded systems in our daily life, the correctness of these systems is becoming a 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 model 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.

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. Reading list will be announced soon. In addition:

The following tools/projects are central to the second half of the class:

Lecture Slides