Software testing/debugging is extremely time consuming, and hence techniques to automate debugging or program repair are of value. In this talk, I will discuss the use of symbolic execution for software testing, debugging and repair. If the correctness criteria for the given program is described by a set of test cases, we will show that symbolic execution methods can help uncover a glimpse of the intended program behavior in various set-ups. It is the uncovering of this intended behavior which can help automate the debugging and repair process. Uncovering of the intended behavior, on the other hand, achieved largely by symbolic execution grouping together many “similar” behaviors.
In this talk, I will start with symbolic execution based test generation and explore various notions of “similarity” which go beyond path coverage based testing. We will explore coarser notions of similarity where collections of paths will be placed in the same partition (deemed similar) in an on-the-fly exploration. Subsequently, I will discuss briefly how such coarser-grained notions of similarity can help symbolic execution based debugging methods that we had studied earlier. Finally, I will spend the bulk of the time on program repair – focusing on one specific symbolic reasoning based repair technique called SEMFIX which has been recently proposed by us. This approach is based on repairing a program with a given test-suite. The talk will keep on returning to the theme of what roles symbolic execution can possibly play – explicitly or implicitly – in building such techniques for software testing, debugging and repair.