CENTRE FOR FORMAL DESIGN & VERIFICATION OF SOFTWARE

2nd Workshop on
Formal Methods in Safety Critical and Industrial Applications – 2002

(2-5 December 2002, KReSIT Auditorium)

The Schedule

Date: 02^nd Dec. 2002 :

Theme : Software Verification using Theorem Proving

Time	Topic
8.30 to 9.00	Registration
9.00 to 10.00	Inauguration (KReSIT Audi.)
T E A B R E A K
10.30 to 11.30	Introduction to Formal Methods (SR) (KReSIT Audi.)
11.30 to 12.45	Lecture: Introduction to Software Verification and the tools ACE and STEP (Anup) (KReSIT Audi.)
L U N C H B R E A K
14.15 to 16.00	Lab. Session: Preliminary usage of the tools (BS) (IECR)
T E A B R E A K
16.15 to 17.30	Lecture: Introduction to Program Verification (SR) (KReSIT Audi.)
17.30 to 18.30	Lab. Session: Problem solving using the tools (BS) (IECR)

Date : 03^rd Dec. 2002

Theme : Hardware Verification using Model Checking

Time	Topic
9.30 to 11.00	Lecture: Illustrative introduction to model-checking and the tool NuSMV (SC/PKP) (KReSIT Audi.)
T E A B R E A K
11.15 to 12.45	Lab. Session: Preliminary experiments with the tools (AT) (IECR)
L U N C H B R E A K
14.15 to 16.00	Lecture: Basics of Model Checking (SC/PKP) (KReSIT Audi.)
T E A B R E A K
16.15 to 18.00	Lab. Session: Problem solving using NuSMV (AT) (IECR)

18.00 CFDVS project Demos

Date: 04^th Dec. 2002

Theme : Software verification using Model Checking

Time	Topic
9.30 to 11.00	Lecture: Program Derivations (AS) (KReSIT Audi.)
T E A B R E A K
11.15 to 12.15	Lecture: Introduction to Promela and verification using SPIN (Anup) (KReSIT Audi.)
12.15 to 13.00	Lab. Session: Exposure to SPIN (SS/VL) (IECR)
L U N C H B R E A K
14.15 to 16.00	Lecture: Model-Checking Distributed Software (SR) (KReSIT Audi.)
T E A B R E A K
16.15 to 18.00	Lab. Session: Verification using SPIN (SS/VL) (IECR)

20.00 hrs Dinner

Date : 05^th Dec. 2002

Theme : Hardware Verification using Theorem Proving

Time	Topic
9.30 to 11.00	Lecture: Theorem proving using Isabelle, PVS (GS/SC) (KReSIT Audi.)
T E A B R E A K
11.15 to 12.45	Lab. Session: Exposure to Isabelle and PVS (LN/SG) (IECR)
L U N C H B R E A K
14.15 to 16.00	Lecture: Basics of Theorem Proving (GS/SC) (KReSIT Audi.)
T E A B R E A K
16.15 to 18.00	Closing Session (KReSIT Audi.)

Note:

SR:	S.Ramesh	SDD:	S.D.Dhodapkar
GS:	G. SivaKumar	SC:	Supratik Chakraborty
AS:	Amitabha Sanyal	PKP:	P.K.Pandya
Anup:	Anup Bhattacharjee	BS:	Babita Sharma
VL:	Vijaya Lakshmi B.	LN:	Lakshmi Narasu MP
SG:	Shweta Gelhot	AT:	Asutosh Trivedi
SS:	Sampada Sonalkar.

Venue For Lectures/Labs:

Kresit Auditorium

IECR: Institute Electonic Class Room, No: SIC101
Cwing, 1st Floor, KRESIT Building