2nd Workshop on

 

Formal Methods in Safety Critical and Industrial

 

Applications

 

 

2 - 5 December 2002

 

 

Organized by

 

Centre for Formal Design and Verification of Software

 

Indian Institute of Technology, Bombay

 

in association with

 

Tata Institute of Fundamental Research, Mumbai

 

and

 

Bhabha Atomic Research Centre, Mumbai

 

The Centre for Formal Design and Verification of Software (CFDVS) at IIT Bombay has been set up with the broad aim of carrying out research and development in the methods for realization of safety-critical/high integrity/mission critical software and hardware with special emphasis on formal design and verification techniques. One of the major objectives of the Centre is to create infrastructure and develop expertise to carry out verification & validation (V&V) at different stages of software & hardware development and emerge as a leading agency to provide know-how and consultancy for independent V&V (IV&V) for high integrity projects. More details about the Centre may be found in the enclosed brochure. [pdf]

 

This is the second in a series of workshops on formal methods conducted by CFDVS.  The first workshop provided an idea and overview of formal methods. In contrast, the aim of this workshop is to provide detailed knowledge of theory and practice behind formal methods and their use in the verification of hardware and software systems.

 

The workshop is intended for designers and developers working on safety critical applications in sectors such as defense, space, nuclear energy, telecommunications, transport etc.  It is also intended for researchers and academicians with interest in formal methods. Masters and doctoral students are encouraged to attend to get a broad exposure to formal methods and techniques.

 

The workshop will involve tutorial lectures introducing the theory of formal methods and practice sessions in which the participants will have hands-on experience with formal verification tools. We plan to use state-of-the art verification tools like SPIN, FormalCheck, NuSMV, VIS  extensively used in hardware and software industries.  Case-studies involving   application of formal methods to some real systems will also be covered.

 

The Centre is keen on undertaking projects in both hardware and software verification.  For this purpose, a half-day session in the workshop will be devoted to interactive discussion with the participants to learn about the kind of verification problems faced by them and to explore possibilities of setting up some collaborative programmes with the Centre.

 

The tentative list of tutorial lectures is:

 

1.      Introduction to Formal Methods

2.      Theory and Practice of Hardware Verification using Model Checking Techniques (with hands-on tools session)

3.      Theory and Practice of Software Verification using Theorem Proving (with hands-on tools session)

4.      Basics of Hardware Verification using Theorem Proving approaches (with tools session if time permits)

5.      Basics of Distributed Software Verification using Model Checking Techniques (with tools session if time permits)

 

Call for Papers/Posters

 

One workshop session is intended to be devoted to participant presentations on application of formal methods to industrial projects involving design and verification of software and/or hardware. Towards this   end, papers   and   posters   are invited from prospective participants.  Proposals for presentation may be sent to the Convener of the Organizing Committee at the following address no later than Oct 20, 2002.

 

Prof. S. Ramesh

Head, Centre for Formal Design & Verification of Software

Dept. of Computer Science and Engineering

IIT Bombay, Powai

Mumbai 400076.

 

 

Organizing Committee

  

S. Ramesh                    ramesh@cse.iitb.ac.in         IIT Bombay (Convener)

 

S. Chakraborty       supratik@cse.iitb.ac.in         IIT Bombay

 

S. D. Dhodapkar      sdd@magnum.barc.ernet.in       BARC, Mumbai

 

G. Sivakumar         siva@cse.iitb.ac.in           IIT Bombay

 

P. K. Pandya         pandya@tcs.tifr.res.in       TIFR, Mumbai

 

R. K. Shyamasundar      shyam@tcs.tifr.res.in         TIFR, Mumbai

 

Sridhar Iyer            sri@it.iitb.ac.in          IIT Bombay

 

A. K. Bhattacharjee    anup@magnum.barc.ernet.in     BARC, Mumbai

 

 

Registration:

  

To register, fill out the attached form completely and mail to the Convener of the Organizing Committee (address given above) with the registration fees.  A copy  of  the  registration form should also be emailed to the Convener.

 

Registration fees for the workshop are:

 

General Rs. 2500


Students Rs. 200


Last date for registration - 20th November 2002

 

  

Registration includes a copy of the workshop notes, as well as lunch and refreshments on the days of the workshop. Fees should be sent by demand draft payable at a bank in Mumbai and drawn in favor of   Registrar, IIT Bombay

 

Limited  grants  are  available  for  students  and  teachers  from educational   institutions.   The  grants  are  intended  to  cover registration  fees,  travel  (by  Sleeper  Class)  and  part  of local expenses  during the workshop. Participants desirous of availing these grants should write or send email to the Convener through their head of department, at the address given above as early as possible. The deadline for receipt of grant requests is  Oct 20, 2002. Decisions about grants will be intimated by email to the applicants by Oct 25, 2002.

 

Accommodation

  

A  few  rooms  at  reasonable  rates  will  also be made available for workshop  participants  at  IIT  Bombay  Guest House and Staff Hostel. Participants  who  wish  to  avail  of these facilities are advised to register early.

 

 

 

REGISTRATION FORM

 

Name __________________________________________________________________

 

Affiliation _______________________________________________________________

 

Mailing Address __________________________________________________________

 

________________________________________________________________________

 

________________________________________________________________________

 

 Email ______________________________________________________

 

Phone _______________________________  Fax  ______________________________

 

Experience with Verification: Please attach a sheet briefly describing your background and experience in verification highlighting the problems that you faced, if any, during verification of some real systems.

 

This write-up would help us greatly in preparing our lectures and can possibly lead to some collaboration with our Centre.

 

Registration Details:

 

Type of registration                                           General/Student

 

Accommodation required                                  Yes/No

 

If yes, accommodation from________________ to _______________

 

Bank draft details:

 

Draft No.__________________________ Dated ________________

 

Drawn on _______________________________________________________________

(Bank)                                                  (Branch)

 

Would you like to give a presentation at the workshop? Yes/No

 

If  yes, please specify title, a brief abstract and time required (max 20 min), on a separate sheet of paper.

 

 

 

   Signature______________________________ Date______________