Intro to S/W Verification - Spring 03 

Course main site

• http://www.cs.bgu.ac.il/~sv032/

My notes

Posted here for your careful use. Please be critic when reading - files might not reflect last minute corrections nor mistakes found in class. Files are posted here for limited time and are later deleted to reclaim space. Print if you want to keep them.

• Class 1 (+ background for class 2)
• Class 2
• Class 3
• Class 4
• Class 5
• Class 6
• Class 7 (pages 15, 16, 17)
  
• Class 8
• Classes 9+10 notes (part1 + part2) and slides (part1 + part2) - courtesy of Yaniv Saar.
  Class 11 - notes & slides - courtesy of Yaniv Saar.
   
• Messages

Assignments

• Assignment 1 - Due on Thursday 20/3/2003 - Solution
• Assignment 2 - Due on Sunday 30/3/2003
• Assignment 3 - Due on Thursday 10/4/2003
• Assignment 4 - Due on Sunday 11/5/2003
• Assignment 5 - Due on Sunday 8/6/2003
   
• Grades

Admin

Contact Info	http://www.cs.bgu.ac.il/~barnav
Class	Thursday 11:00-12:00, room 90/227
Office hours:	Monday 15:00-16:00

Links

• TLV - Temporal Logic Verifier
• JADE - Implementation and Visualization of a BDD Package in JAVA
• BeanShell - Lightweight Scripting for Java

Downloads

• TLV executable for BGU Sun systems
• TLV rules.tar.Z

Of Interest

• Java Programming With Assertions
   

• Finding strongly connected components in a directed graph:

1) Tarjan's original algorithm

2) from Introduction to Algorithms / T. H. Cormen et. al. (Hebrew edition) - scc algorithm, dfs algorithm.