Pre-Conference
Workshop on Applied Formal Methods
Hyderabad, 14--17 December, 1996
Coordinators:
- USA:
N. Shankar
Computer Science Laboratory
SRI International
Menlo Park, CA 94025
Deepak Kapur
Suny, Albany
NY, USA
- India:
R.K. Shyamasundar
Computer Science Group
TIFR
Bombay 400 005
Purpose of the Workshop
The field of formal methods includes the study of specification
languages and logics and verification methods such as theorem proving and
model checking. Formal methods are increasingly being applied to
the core algorithms in safety critical systems and in
the verification of hardware circuit designs. A workshop on
Applied Formal Methods is being organized in Hyderabad, India,
in December 1996. The goal of this workshop is to bring together
several international experts in the U.S., India, and elsewhere
with domain experts from Indian academia and industry.
The workshop is aimed at promoting a healthy exchange between
international formal method experts and domain experts in India.
The main motivation for the workshop is:
- A fruitful exchange of ideas and technologies among the various
formal approaches, verification systems developers, and applications
experts.
- A discussion of the best scientific techniques for the
specification, design, and analysis
that can help avert Bhopal-scale disasters in the development
of complex hardware and software systems.
Workshop Topic.
Digital hardware and software systems pose serious engineering
challenges. These systems are increasingly being used in
safety-critical contexts where even small errors or modifications
to these systems can have large consequences. The complexity of
digital systems has clearly outpaced the ability of existing
design methods. This is evident in the rising anecdotal evidence
of important failures resulting from software or hardware bugs:
the Intel FDIV error, the crash of the AT\&T switching network,
the fatal over-radiation problem with the Therac-25, among many
others. Formal methods provides a scientific foundation for the
development of digital systems by way of specification languages
and logics, formal design methodologies, and mechanized
analytical tool support. Formal methods technologies have only
recently begun to demonstrate the maturity needed for significant
industrial application. There are now several very capable tools
and methodologies that have been successfully field-tested on
large-scale applications of processor designs and safety-critical
algorithms.
The international workshop on Applied Formal Methods is
being organized be held at Hyderabad, India, in December 1996, in
conjunction with the international symposium on Foundations of
Software Technology and Theoretical Computer Science (FST&TCS)
sponsored by the Indian Association of Research in Computing
Science. The workshop is being supported by NSF, USA.
Main Topics:
- Safety-critical system issues
- Formal Methods issues
- Automated reasoning
- Induction
- Model checking
- Real-time systems
- Reactive Systems
- Synchronous Languages
- Hardware verification
Confirmed Speakers
- John Rushby, SRI International
Formal Methods and
Safety-critical systems
- J. Moore ( Computation Logic Inc, Texas)
Theorem
proving and System Verification
- Deepak Kapur ( SUNY Albany)
Automated Theorem Proving
- Rajeev Alur (Bell Laboratories)
Real-time systems
- J. Sifakis (Verimag, Grenoble)
Model Checking
- Natarajan Shankar (SRI International)
Mechanized
verification
- RK Shyamasundar (TIFR)
Synchronous/Reactive Systems
- G. Huet (INRIA)
Proof Checking
- A. Pnueli (Weizmann Institute, Israel)
Temporal/Program Logics
- M. Srivas (SRI International)
Hardware Verification
In addition, a couple of more speakers are expected.