Verification, Testing and Statistics

December 3, 2009

Sriram Rajamani


Verification, Testing and Statistics

Time:   11:00am
Location:   IMDEA conference room

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