Program Verification Notes

Automated Program Verification

Description (Short)

Program verification is a correctness assurance method based on mathematical models of programs. It is superior to testing because of its precision and its ability to represent an entire range of test cases (even infinitely many of them!) with only a few mathematical formulas. In this course the student will be introduced to three techniques in program verification: model checker, theorem prover, and abstraction.

Description (Long)

Critical errors are errors made by a computer system that have costly consequences. As our society become increasingly dependent on computers, the risk of having critical errors also increases. It becomes increasingly urgent to ensure that our software, especially those deployed to handle critical tasks, meet a high standard of correctness. Without doubt, this is going to cost us something. The traditional way of assuring software correctness is testing. Testing is inexpensive. Unfortunately, testing becomes increasingly unadequate.

Program verification is another approach in correctness assurance. Verification is based on mathematical models of programs. It is superior to testing because of its precision and its ability to represent an entire range of test cases (even infinitely many of them!) with only a few mathematical formulas. However, its reliance on mathematics makes the approach expensive and rather unaccessible for ordinary programmers. Still, it is a very potential approach, and depending on the application domain and the ammount resources that a company has, verification may be an attractive solition. It is also a very active research field. People keep coming with new innovations, and there are already many tools to automate many tasks and make verification a lot cheaper that it used to be ten years ago.

In this course the student will be introduced to three techniques in program verification: model checker, theorem prover, and abstraction. Model checker is a push button (fully automatic) technology, though its language is limited. Theorem prover on the other hand, is extremely expressive, but it is only semi automatic. Abstraction is a pre-processing technique which is necessary to handle realistic programs by deriving simpler models which are more tractable for either model checkers or theorem provers.

Tools

We are going to use the following tools:

1. Model checker: Spin
2. Theorem prover: HOL
3. Abstraction: xMECH-HOL

Course Format

Lectures, tutorial, training, and programming assignments.

Grading

Based on the assignments.

Requirement

1. Basic course in mathematics [B&B]. The student is assumed to be familiar with the notions of set, function, and relation.

2. Basic course in predicate logic [B&B].

3. Basic course in programming logic for sequential programs [P&C] (e.g. Hoare-triple based logic, assertional logic)

4. Functional programming [FP]. The student is assumed to be familiar with Haskell- or ML-like type systems.

5. Basic course in language and grammar [GnO]. The student is assumed to be familiar with context free grammar, BNF notation, and the notion of abstract syntax.

Required Logistic

• 28 contact slots, each slot is 2 x 45 minutes, preferable with flexible partition into lecture and lab slots. It is prefereable if the lab slot is allocated after and in the same day as the lecture slot.

• lab with UNIX or windows system with Spin and HOL taupo installed. xMECH will be provided as downloadable ML source.

Plan

L = lecture (college)
T = training/tutorial (werk-college)
A = programming assignment (practicum)

Total requested contact slots: 14L + 14T/A. Change?

Total in plan: 9.5L 5T 12A

1. Basic [1L,3T fit in 1 whole week]
   1. [.5L] Review on Hoare logic
   2. [.5L,1T] Writing formal specifications
   3. [2T] Refresh training: Constructing formal proof

2. Model checking [4L + 4A]

3. Theorem prover [3L,2T,4A]
   1. [.5L] Quick introduction to programming in ML
   2. [.5L] HOL: language & basic proof rules
   3. [1L] HOL: tactical language & subgoal package
   4. [1T] Tutorial 1: specififying and verifying with HOL
   5. [1T] Tutorial 2: embedding (parity checker)
   6. [4A] Assignment: specifying and verifying programs with HOL
   7. [0L] HOL Tips
   8. [1L] HOL Meson and Rewrite tools

4. Abstraction [1.5L, 4A]
   1. [1L] Implementing a simple programming language and logic in xMECH
   2. [4A] Assignment: make the inference engine smarter
   3. [.5L] [optional] PLGA part of xMECH.

-- WishnuPrasetya - 06 Mar 2002