Research

I have a keen interest in exploring data-structures -- studying their strengths and weaknesses so that I can use them effectively when needed. I'm also a follower of developments in AI and Distributed Systems since I find many of these techniques useful in my work.

Theorem-Proving

My interest in formal software verification techniques was piqued after working with Dr. Simanta Mitra on a tool to automatically generate proof-obligations for a subset of Java annotated with JML -- developed at Iowa State University under Dr. Gary Leavens. If these proof-obligations can be proved -- either by hand or using a theorem-prover -- then certain claims could be made with regards to the annotated system.

Model-Checking

I've since moved on the field of model-checking. Some of the more interesting problems I have come across deal with storing large sets of numbers (that could for example represent a function) and then being able to efficiently manipulate these data-structures.

Of specific interest to me are Decision Diagrams. Lately, Ordered Binary Decision Diagrams (OBDDs) have helped increase the size of systems that can be analyzed by model-checkers by an order of magnitude. I am working with Dr. Andrew Miner and Dr. Samik Basu on building a library to build and analyze a recent cousin of OBDDs -- Multi-valued Decision Diagrams (MDDs). Details about this library and related-work can be accessed via Andy's pages.