Parameterized unit tests

Nikolai Tillmann, Wolfram Schulte
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 07 September 2020

Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering
Lisbon, Portugal
Association for Computing Machinery
New York, NY, USA
Pages 253-262
Note(s): symbolic execution, unit tests, property-based testing, SMT solver

Parameterized unit tests are a form of property-based testing that generalizes traditional unit tests. The tests can be instantiated with concrete values to serve as traditional tests, they can be verified using symbolic execution or, to support modular verification, they can be used as axioms in the spirit of algebraic specification to use when verifying calls to a library.

This was implemented for .NET on an early symbolic execution tool using early SMT solvers. It is evaluated on eight benchmarks (qsort, triangle, hashtable, bad, linkedlist, red-black tree).

The paper has a lengthy related/future work section that cites lots of early (forgotten?) work on test generation from formal specifications from the ’90s.