In recent years, there have been significant advances in symbolic execution technology, driven by the increasing maturity of SMT and SAT solvers as well as by the availability of cheap compute resources. This technology has had a significant impact in the area of automatically finding bugs in software. In this tutorial, we will review ways in which symbolic execution can be used not just for finding bugs in programs, but also in debugging them! In current practice, once a failure-inducing input has been found, humans have to spend a great deal of effort in determining the root cause of the bug. The reason the task is complicated is that a person has to figure out manually how the execution of the program on the failure-inducing input deviated from the intended execution of the program. We will show that symbolic analysis can be used to help the human in this task in a variety of ways. In particular, symbolic execution helps to glean the intended program behavior. We will show that this ability of symbolic execution in extracting program specifications can help in automating program repair as well. Concretely, the tutorial will provide a background in symbolic execution, and then cover material from a series of recent papers on determination of root cause of errors and their repair using symbolic techniques, such as [1, 2, 7, 5, 4, 6, 3]. This is an emerging area, and the tutorial will point out opportunities where additional research is needed. This tutorial will further link up the software engineering community with programming languages and formal methods, in the context of software debugging and repair.
Mon 26 Oct
|13:30 - 15:00|