IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2009 > Verification, Testing and Statistics

Sriram Rajamani

Thursday, December 3, 2009

11:00am IMDEA conference room

Sriram Rajamani, Researcher, Microsoft, India

Verification, Testing and Statistics

Abstract:

We present work by the RSE group at MSR India. We start by describing Yogi, a property checker that combines static and dynamic analysis. Then, we move beyond verification and testing and look at broader problems. Program Analyses either static or dynamic have traditionally analyzed only code. However, we have a lot of data 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 the program together with analysis of such data, we can solve very interesting new problems. We present 3 such tools based on this general theme:

  • Merlin: which combines static analysis with probabilistic inference to infer security specification inference, and find security errors in programs
  • Holmes: where we use path profiling together with a statistical model to find root causes of errors
  • DebugAdvisor: where we use data from version control, bug databases etc, and combine information retrieval together with tricks specific to programmatic structures and find relevant information for people doing debugging