Symbolic Execution for Evolving Software

Abstract

One of the distinguishing characteristics of software systems is that they evolve: new patches are committed to software repositories and new versions are released to users on a continuous basis. Unfortunately, many of these changes bring unexpected bugs that break the stability of the system or affect its security. In this talk, I describe our work on devising novel symbolic execution techniques for increasing the confidence in evolving software: a technique for reasoning about the correctness of optimisations, in particular those that take advantage of SIMD and GPGPU capabilities; a technique for high-coverage patch testing, and a technique for revealing regression bugs and behavioural divergences across versions.

Talk given at ETH Zurich, Chair of Programming Mehodology.