A case study in Non-Functional Regression Verification

In the process of software evolution, it is an important concern to prevent the introduction of unwanted behavior or bugs (known as regressions) due to updates or when a new feature is implemented in the software. Regression testing is one common solution to identify regressions; a complementary approach that has the same goals as regression testing, but applies methods from formal verification is called regression verification. Usually, both regression testing and verification only consider functional properties, e.g., the results produced by a program. In this thesis, non-functional regressions are considered, in particular detection of modifications that adversely affect program run-time. Applying the method of regression verification, it is shown that two versions of a program produce the same output for all inputs, as well as verified that the two versions are equal with respect to run-time. For the latter step, programs are instrumented to count the number of executed instructions (weighted by the cost of instructions); those counters can then be compared using functional regression verification. Experiments show that this combination of functional regression verification and instrumentation can effectively analyze non-functional Equivalence properties for a range of example programs. In the experiments, the REVE tool, is used to determine functional equivalence after instrumentation