Ongoing Funded Research Projects

  1. Centre for Formal Design and Verification of Software

    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 ( gives more details of our activities.

  2. Test Vector Generation for i960 Microprocessor

    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.

  3. Formal methods for Policy based Network Management

    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.

  4. Code Optimization for Ultra-Sparc

    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.