Untitled

                                                                            Introduction to Software Verification
                                                                                     212-1-5131
                                                                                                      Wed. 17.00 - 20.00
                                                                                                     Building 34, Room 116

Instructor: Yonit Kesten

e-mail: ykesten@bgumail.bgu.ac.il

office: Nihul, 132

office hours:

TA: Barak Naveh

            e-mail at: http://www.cs.bgu.ac.il/~barnav/
                phone:    08-6477828
                office:
                office hours:

Bulletin Board

Lectures and Assignments

Week	Topic - main	Subtopic	References	Slides	Tutorial	Assignmemts
1 (26.2)	*Verifying Sequential Programs*	Introduction	F chap 2 + sections 3.1-3.3	slides(ppt) slides (ps) slides (pdf)	FlowChart Programs Partial Correctness - Example.	A1
2 (5.3)		Floyd partial correctness		slides (ps) slides (pdf)
3 (12.3)		Cutpoints independence		slides (ps) slides (pdf)		A2 Cutpoint independence Proving success Finding invariants
4 (19.3)		Completeness of partial correctness Proving success Inductive assertions		slides (ps) slides (pdf)
5 (26.3)		Proving convergence		slides (ps) slides (pdf)		A3 Proving Convergence
6 (2.4)		Hoare Logic		slides (ps) slides (pdf)	Preparing for the BDD assignment
7 (11.4)	*Verifying Concurrent Programs*	Textual programs(continued) BDD's		slides (ps) slides (pdf) BDD-notes (ps)	BDD's	A4(a) - BDD's basic implementations
8		BDD's		slides-a (ps) slides-a.pdf slides-b (ps)	BDD's	A4(b) - BDD's operations
9		Concurrent programs and their computation model example of incorrect programs		slides (ps) slides (pdf)	TLV	A5
10		*Enumerative* model checking		slides (ps) slides (pdf)	TLV
11 (4.6)		Review lecture 10 *Symbolic* model checking		slides (ps) slides (pdf)	Symolic model checking	A6
12 ?		Testers Verifying general temporal properties		-----------

TextBooks:

Part I: Verifying Sequential Programs:

Program Verification, by Nissim francez, Addison-Wesley 1992. (F)

Part II: Verifying Concurrent Programs:

Temporal Verification of Reactive Systems. Safety, by Manna and Pnueli, Springer Verlag 1995. (P)
Model Checking, by Clarke, Grumberg and Peled, MIT Press 1999. (C)

Syllabus

Grading:

-- 20% home assignment. 80% final exam.

-- Must pass the final exam with grade 56 and up.

Acknowledgement

he slides of Part I of the course are taken from a course presented by Prof. Amir Pnueli

slides (ps)-a

slides (pdf) - b