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.
|