When: Friday, May 09, 12:00 p.m.

Where: 4623 Wean Hall

Robert J. Simmons

Speaking Skills Talk

Abstract:
Microsoft Research India's Yogi Project combines two technologies, counter-example guided abstraction refinement (CEGAR) style software model checking and automatic test case generation, with the aim of increasing the power and efficiency of proving properties of C-style programs. Yogi integrates both techniques by using the program abstraction to guide testing and using the results of symbolic execution to generate the counterexamples that guide graph refinement, in many cases allowing the tool to succeed more efficiently than possible with either technique alone. I will describe the Yogi algorithm and an extension that allows it to efficiently cope with C programs without relying on any whole program alias analysis.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

<< Back