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.