My main research interests are formal methods to analyse complex programs, such as Model Checking and Theorem Proving. Much of my current work is dedicated to curbing the verification complexity associated with replication, which is one of the most common design patterns for concurrent systems. My approach is to exploit regularity that many such systems exhibit. At an abstract level, systems with replicated components can often be described very compactly. If the regularity is recognized at this level, we may be able to avoid the complexity due to replication altogether.
Further academic interests include theoretical aspects of computer science, including the theory of computability and computational geometry, here especially the art of discretizing continuous geometric problems.
I received a doctoral degree in Computer Sciences in 2007 from the University of Texas at Austin. My supervisor was E. Allen Emerson. Before joining OUCL, I spent about a year and a half at The Swiss Federal Institute of Technology (ETH) in Zurich.
