| Summary: | Software plays an important role in everyday life, from consumer applications to mission-critical systems. This richness of functionality, however, comes at the price of complexity. Even though software systems are developed manually, they are increasingly too complex to be fully understood by any single programmer. As a consequence, software bugs, which are often the result of programming errors, are commonplace. In this thesis we present two techniques based on dynamic symbolic execution which address the problem of software reliability from two angles: testing software patches and recovering an incorrect program input. We present shadow symbolic execution, a technique that generates test inputs exercising the new program behaviours introduced by a software patch. The old and the new version are executed in the same symbolic execution instance, with the old version shadowing the new one. Whenever the versions diverge at a branch point, we generate an input exercising the divergence and comprehensively test the new behaviours of the new version. We evaluate our technique on a set of incorrect patches from GNU Coreutils for which it generates inputs that exercise newly added behaviours and expose some of the regression bugs. We also present Docovery, a novel document recovery technique that makes it possible to fix broken documents without any knowledge of the file format. Starting from the code path executed when processing a broken document, Docovery explores alternative paths that avoid the error, and makes small changes to the document in order to force the application to follow one of these alternative paths. We evaluate Docovery on files processed by several popular applications: the e-mail client pine, the pagination tool pr and the binary file utilities dwarfdump and readelf. The thesis also includes a motivational large-scale study on the correctness of PDF documents and document readers.
|
|---|
