Improving the Robustness of Regression Test results

Introduction

Regression tests are a useful way of helping ensure that incremental software upgrades are suitable for release. For example, a regression test suite is commonly used to test a candidate patch is suitable to be committed to a version-control repository. Our group develops several tools for software verification, and these each have test suites designed to ensure the correct functionality of the software on a collection of verification examples. However, the results of these system tests are usually checked by a simple string comparison with an expected result. This leads to test results which are far too brittle with respect to harmless modifications. For example, changing the formatting of an example or adding extra comments may change the line numbers on which certain (perhaps expected) errors are reported. Similarly, fixing spelling mistakes in the wording of the errors themselves, could also cause regression tests to fail unexpectedly.

Goal

The goal of this project is to develop and implement a more-robust mechanism for automatically evaluating regression test results from our verification tools. This will involve choosing a suitable annotation syntax (initially for Boogie programs), and implementing the extraction of expected test results from these annotations. The annotations will be designed to give results which are suitably abstract, e.g., using pattern-matching to identify only certain expected substrings, or by using enumerations to identify a particular class of error message. It may also be desirable to support parameterised descriptions – for example, to allow to specify not just that a particular message is expected, but that it is expected to mention particular program variables x and y, etc. The implementation can be evaluated by replacing the existing regression testing mechanisms.

Recommended Background

• Interest in Formal Methods / Program Verification
• Programming Experience

Contact

Alex Summers or Valentin Wüstholz