Centre for Formal Design and Verification of Software

IIT Bombay

The crucial role of software engineering based on formal methods for design and verification of safety-critical software was the major motivation for the Department of Atomic Energy to establish the Centre for Formal Design and Verification of Software (CFDVS) at IIT Bombay. CFDVS started functioning in 1999 as a collaborative effort between IIT Bombay, Tata Institute of Fundamental Research (TIFR) and Bhabha Atomic Research Centre (BARC). Since then, it has established itself as a national R&D Centre in the area of verification of high-integrity software and hardware. The research and development activities at CFDVS has resulted in the development of several prototype tools that have been used to solve industrial scale problems. The research work that led to the development of these tools have also been disseminated through several publications in reputed international conferences and journals. The Centre has successfully executed projects from Government R&D Centres like VSSC, BARC, DRDL and ADA. It also attracted funded projects from many private sector companies such as Texas Instruments, Microsoft Research India, Intel Corporation, and General Motors.

Major completed and ongoing projects at the Centre include

  • Assertion checking environments (ACE, ACE-II) for C programs
  • Bounded model checker for VHDL designs
  • Parallel model checker for hardware designs
  • Static analyzer for C programs combining multiple abstract interpreters
  • Framework for modeling and analysis of requirement specifications of systems
  • Word-level symbolic trajectory evaluator for SystemVerilog designs
  • Constrained test generation tools with guarantees of uniformity
  • Tools and techniques for formally analyzing and verifying software product lines
  • Parallel synthesis of boolean functions from relational specification
  • Network analysis tool for analyzing gene regulatory networks for use in systems biology