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
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)
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.
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.
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______________