Corina Pasareanu and I were just awarded the 2007 HVC Award for the "most promising contribution(s) to verification published in the last year"
I'm now working as a Senior Software Engineer at SEVEN Networks and am no longer at NASA. SEVEN is the leading provider of software for making email work on mobile phones. I'm working on the scalability and reliability of their server side software. Well that was the idea anyway, turned out that I'm spending a great deal of time on data mining to determine how our software can be improved. It is quite interesting how good a debugging tool a database and SQL is: often times strange data is pointing to some bug in the code. I'm also just started doing load testing and this is actually more difficult than I first assumed. For load testing one needs to understand all of the system in great detail, which means one actually needs to understand the system better than the original developers (since they tend to know only the components they worked on!). I'm still going to have one foot in research and will be writing papers and attending conferences. Interesting also how my focus at conferences have changed - now when I see some cool research I'll dismiss it immediately if it is too immature for the real-world. BTW, if you are looking for a job at SEVEN, let me know, we are growing and need good people.
During my time as a contractor at NASA I was employed by RIACS (Research Institute for Advanced Computer Science) and conduct my research within the Robust Software Engineering group at NASA Ames. I obtained an M.Sc. from the University of Stellenbosch in South Africa (1993) and a Ph.D. from the University of Manchester in the UK (1998).
My, pre-SEVEN, research focused on doing model checking for actual programs and more specifically I'm working on Java PathFinder , a model checker for Java. My research is slowly tilting towards testing and to that end we have extended JPF with a symbolic execution capability that allows us to reason over symbolic data and symbolic structures. The main application off the new JPF is to do test-input generation in both a black- and white-box fashion.