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

Where: 4623Wean Hall

Robert J. Simmons, Computer Science Department

SCS Student Seminar Series

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 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.

<< Back