Bug Finding Techniques for Programs with Infinitely Many States

  • Pierre Ganty | IMDEA Software Institute

I will introduce a bug finding technique for concurrent programs over a finitized data domain and a general framework for underapproximations arising from it. Then, I will move to sequential recursive programs over the integers and present a novel underapproximation technique capturing executions with unbounded stack usage. All those algorithmic techniques distinguish by offering extended coverage compared to the state-of-the-art.

Speaker Details

Pierre joined the IMDEA Software Institute in September 2009 after completing a nearly two years postdoc at the University of California at Los Angeles, USA. He holds a joint PhD degree in Computer Science from the Université Libre de Bruxelles, Belgium and from the Universitá Degli Studi di Genova, Italy that he obtained late 2007.
His research interests include algorithmic verification of systems with infinitely many states, algorithmic model based bug finding and automatic refinement of abstract domains.

Series: Microsoft Research Talks