2nd Workshop on


Formal Methods in Safety Critical and Industrial





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




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





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.




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.






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______________