Regression verification has been proposed as an alternative to regression testing to combat the drawbacks of the latter. Using regression verification, a verification task is employed to formally prove that an incremental change does not disturb established software behaviour. The benefits of this approach include that, for reasonably confined modifications, verification may be less costly than creating, maintaining, and running a large curated test suite. This gives regression verification the significant potential of reducing software production costs, increasing productivity and trust within development teams, and supporting high-frequency codebase modifications.
Regression verification is often performed using program equivalence verification techniques (e.g., see RVT, LLREVE) which can guarantee (in several examples) that two pieces of code have the same observable behaviour.
The topic of this project is to create an inequivalence finding tool for code using Fuzz Testing (i.e random test generation). In contrast to equivalence verification this tool will not guarantee equivalence but it may be very efficient in finding inequivalences with very limited user guidance. In other words this will be an automatic bug-finding tool with respect to program equivalence.
There are two potential projects in this topic.
- One of the projects will develop this technique in a small ML-like language and compare the results with the equivalence verification tool called Hobbit, in development at TCD [publication]. Here, qcheck or a similar tool for OCaml/ML will be leveraged to implement random testing. The resulting inequivalence-finding tool will be compared with the equivalence-verification tool Hobbit.
- The other project will develop the technique in Java and will use the JQF tool for implementing fuzz testing. It will also extend previous work by an MSc project.