Home  I   Research   I   Publications   I   Other    

Formal Verification:

Within Formal Verification the following topics are most relevant to my work:
  • Model Checking
  • Abstract Interpretation
  • Protocol Verification
  • Compositional Reasoning
  • Decision Procedures
  • Theorem Proving

Current project:

My work in the recent years has focussed on verification of concurrent and distributed protocols like cache coherence protocols, mutual exclusion protocols that form the bedrock of modern multi-processor systems. Apart from the inherent parallelism, these tend to be very intricate (so as to get maximum performance out of them) and consequently susceptible to subtle bugs. Techniques like testing and simulation, which only provide partial system coverage, are usually inadequate in dealing with complex distributed systems.

A recent technique developed by us at SCL allowed us to verify state of the art cache coherence protocols developed at Intel in full generality and with a high degree of automation (see our FMCAD 2008 & 2009 papers for more details). There probably isn't any other method capable of handling industrial protocols at such level of automation.

Non-FV work:

As a part of my under-graduate thesis on DNA Computing, I showed that a splicing based string generation mechanism (technically SEH(2,3)(p)) is equal in power to a context free grammar. This resolved an open problem  regarding the power of splicing systems (see Gh. Paun, G. Rozenberg, A. Salomaa. DNA Computing, pages 264-266) and completed the task of characterizing the power of splicing systems.