Funded by Govt. of India.

I am one of the two principal investigators from IIT Bombay on a project funded for 4 years from March 1999. (to the tune of Rs. 3 crores- US$ 0.6 million) for the use of Formal Methods in specification and verification especially for safety-critical applications. The Centre's home page (http://www.cfdvs.iitb.ernet.in) gives more details of our activities.

Funded by ISRO, Trivandrum.

The aim of this project is to generate test sequences that can be used for screening the Intel 80960 processor chips to be used in on-board computers. This involves the following steps.

1. Development of correct and fault models of the processor,
2. Generation of test sequences, in the form of instruction streams that can reveal the modeled faults,
3. Conversion of the the test instructions into HP tester input format.

Funded by Switch-on Networks, USA.

Policy based network management is a promising approach for effective management of bandwidth, QoS and security of a complex network. Towards building such systems, Policy Specification languages for formulating policies are needed. The specification methodology should be adequately expressive, easy to use and also allow policy specifications to be automatically translatable into an implementable framework. Even more important, it should have a clean underlying formal model and semantics which allows automated verification of properties such as policy consistency, completeness and conflicts. This project will explore the use of equational logic framework for specification and analysis of network policies and build the required tools for demonstrating feasibility of this approach.

Funded by Sun Microsytems, USA

The high performance of today's super-scalar processors can be attributed to their ability to issue more than one instruction per clock cycle. Optimizing compilers should ideally exploit this Instruction Level Parallelism to improve the performance of programs. Software pipelining is a popular loop optimization technique which exploits ILP. However, there are certain constraints, like data dependences, memory bottleneck, hardware resources, which may prevent the optimal performance of software pipelining. This project explores the various constraints and studies the impact of these constraints on software pipelining.