Verification-Aided Regression Testing (VART) is a novel extension of regression testing that has a fault revealing capability that is significantly less sensitive to the completeness of the validation test suite due to the use of model checking.

VART can automatically detect regression faults not detected by regression test suites.

VART output is a list of program properties valid for the base version of the software but no longer valid for the upgraded version. Like the following:

  • src/store.c  available_products  assert( return >= 0 );
  • src/store.c  31  assert( total >= 0 );
  • src/store.c  28  assert( total >= 0 );

The key idea in VART is to extend the use of test case executions from the conventional direct fault discovery to the generation of behavioral properties specific to the upgrade, by:

  • automatically producing properties that are proved to hold for the base version of a program;
  • automatically identifying and checking on the upgraded program only the properties that, according to the developers’ intention, must be preserved by the upgrade;
  • reporting the faults and the corresponding counter-examples that are not revealed by the regression tests.

VART has been presented at ISSTA 2014. The scientific paper describing VART can be downloaded from the following URL

VART has been partially supported by the EU Community under the call FP7-ICT-2009-5 project PINCETTE 257647. More info about the EU project Pincette available at the following URL: