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: 02nd 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 : 03rd 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: 04th 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 : 05th 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