My current research interests are split between techniques for formally verifying hardware and software, plus a new style of parallel computing we call Data-Intensive Super Computing.
In formal verification, we have developed a number of methods over the years for representing system operation, specifying desired properties of the system, and then either proving the system satisfies the properties or determining ways it can fail. Much of our success has been built on methods for representing and reasoning about Boolean functions. Most recently, we have raised the level of abstraction up to word-level models, viewing a word as either a bounded or unbounded integer. Our work combines modeling, verification tools, and ways to reason about the underlying logic.
Data-Intensive Super Computing, or "DISC" seeks to create a class of systems that will enable computing over massive data sets. Currently, systems of this type are created by Google and its competitors to support web search, but we believe the ideas can be applied to many other domains, including computational biology, medicine, and commerce. It will involve research activities in system design, programming models and languages, parallel algorithms, and application areas such as machine learning and natural language processing.