2nd Workshop on
Formal Methods in Safety Critical and Industrial
2 - 5 December 2002
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)
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
S. Ramesh firstname.lastname@example.org IIT Bombay (Convener)
S. Chakraborty email@example.com IIT Bombay
S. D. Dhodapkar firstname.lastname@example.org BARC, Mumbai
G. Sivakumar email@example.com IIT Bombay
P. K. Pandya firstname.lastname@example.org TIFR, Mumbai
R. K. Shyamasundar email@example.com TIFR, Mumbai
Sridhar Iyer firstname.lastname@example.org IIT Bombay
A. K. Bhattacharjee email@example.com 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.
Mailing Address __________________________________________________________
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.
Type of registration General/Student
Accommodation required Yes/No
If yes, accommodation from________________ to _______________
Bank draft details:
Draft No.__________________________ Dated ________________
Drawn on _______________________________________________________________
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.