Symbolic Execution for Evolving Software

Cristian Cadar

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 two techniques based on symbolic execution for checking the correctness of evolving software: a technique for automatic testing of code patches, which combines symbolic execution with several novel heuristics based on static and dynamic program analysis; and a technique that combines symbolic execution and crosschecking to test and verify the correctness of optimizations such as SIMD and GPGPU optimizations.

--
Cristian Cadar is a Senior Lecturer in the Department of Computing at Imperial College London, where he leads the Software Reliability Group (http://srg.doc.ic.ac.uk). His research interests span the areas of software engineering, computer systems and security, with an emphasis on building practical tools for improving the reliability and security of software systems. Cristian received a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology.