Verification, Testing, and Statistics

Over the past decade several static and dynamic analysis tools have emerged to help programmers find errors in programs before their customers encounter them, or worse, before hackers find them and exploit them! We give a tutorial introduction to how these tools work. We cover three generations of such tools developed at Microsoft Research: Heuristic tools (for example, Prefix, Prefast), Sound tools (for example, SLAM), and Directed testing tools (for example, DART, Yogi), as well as trace the progression of how these tools have evolved over the past decade.

We then talk about a more recent trend, where we are starting to exploit data we have about our software—ranging from data about our development processes, including bug databases and version control, to data from profiles of runs, to data about how users use the software. If we combine analysis of programs together with analysis of such data, we can solve very interesting new problems. We present recent research in this direction.

Sriram Rajamani is Assistant Managing Director of Microsoft Research India. In addition, Sriram leads the Rigorous Software Engineering (RSE) group in Microsoft Research India. Sriram's research interests are in programming languages and programming tools. Sriram has a PhD in Computer Science from the University of California at Berkeley, MS in Computer Science from the University of Virginia, and BE in Computer Science from Guindy College of Engineering, Chennai. In a previous life Sriram has worked as a programmer for over 5 years writing telecommunication software (for Syntek Inc) and electronic design automation software (for Xilinx Inc). He uses his first-hand experience in the realities of commercial software development to guide his choice of problems and approaches to research in software productivity.