The Formal Verification Research Group at the Dept. of Computer Science & Engineering, Indian Institute of Technology Kharagpur has more than ten years of experience in the development of formal and semi-formal validation technology. The group engages in fundamental research to solve emerging challenges in design validation and provides solutions to industrially relevant validation problems.

NEW !! Open Positions For Ongoing and Forthcoming Projects

Focus Areas (click on the topics for details)

Recent Publications    Tools      Group Members
Partners in Sponsored Research       Contact
 

Group members

  Pallab Dasgupta       P.P.  Chakrabarti

  Research students (PhD.) :

  1. Priyankar Ghosh
  2. Kamalesh Ghosh
  3. Aritra Hazra
  4. Antara Ain
  5. Sumana Ghosh
  6. Rajorshee Raha
  7. Kajori Banerjee

  Research students (M.S.) :                        

  1. Rajdeep Mukherjee

 Former Members :
    Srobona Mitra                     Subhankar Mukherjee         Padmalochan Bera               Sourasis Das                 Debjit Pal                                Manoj Dixit
    Arijit Mondal                      Sagar Chaki                           Pankaj Chauhan                   Shuvendu Lahiri         Jatin Deka                               Arindam Chakrabarti
    Diganchal Chakraborty     Krishnendu Chatterjee        S. Sriram                                Anirvan Dasgupta       Indrajit Bhattacharya            A. C. Pathak
    Sandeep Chakrabarti          Pritam Roy                            Samik Das                             Subhojit Basu              Prasenjit Basu                         Sayantan Das
    Ansuman Banerjee             Suchismita Ray                    Anindya Sundar Nandi       Bhaskar Pal                   Rajdeep Mukhopadhyay     Sayak Ray

Partners in Sponsored Research

Tools

Recent Achievements:
 

  • Incorporating formal methods to enhance the speed of logic evaluation in Verilog Cycle Simulators
  • Development of tools and technology for formal property verification in modules under specified

    •    environment models. We have implemented model checkers that check both untimed as well as
       real time properties on open systems (modules).
  • Development of temporal logics for efficient verification of timing properties. We have shown that

    •    reasoning about extremal (best case/ worst case) timing properties is   tractable in practice, where as,
       it is known that model checking timed logics are PSPACE complete or harder in general.
  • Development of a validation platform for high level SOC designs specified in SDL augmented with System C.
  • Development of Open Vera Assertion (OVA) checkers for standard BUS protocols
  • Reasoning about the coverage of architectural level correctness properties by RTL correctness properties.

    •    

    Contact:
    Dr. Pallab Dasgupta,                                                       Phone: +91-3222-283470
    Professor,                                                                          Fax:    +91-3222-278985
    Dept. of Computer Sc. & Engg.                                   Email: pallab@cse.iitkgp.ernet.in
    Indian Institute of Technology,
    Kharagpur, India-721302

     List of Conferences