“Can structural test adequacy criteria be used to predict the quality of generated invariants?” by Soroush Karimi Rad. Masters thesis, University of Antwerp Department of Mathematics and Computer Science, (Antwerp), 2005.
The use of invariants during software development has many advantages. Among other things, invariants can be used to formally specify programs, to check certain vital properties at run-time, improve communication between programmers and make understanding programs easier. Despite these advantages, many programs lack explicit invariants. Dynamic invariant generation can automatically derive invariants from the program source but needs an initial test suite. Moreover, the quality of the generated invariants depends on this initial test suite. Many programs have test suites for detecting errors which are designed according to structural coverage criteria. In order to reuse these test suites for invariant generation, we must investigate the ability of structural coverage criteria to produce good quality invariants. An experiment was setup to investigate this ability. Our results indicate that there is indeed a correlation between structural coverage criteria and the quality of the generated invariants, but that in some cases this correlation can become weak due to other factors.
BibTeX entry:
@mastersthesis{Rad2005, author = {Soroush Karimi Rad}, title = {Can structural test adequacy criteria be used to predict the quality of generated invariants?}, school = {University of Antwerp Department of Mathematics and Computer Science}, address = {Antwerp}, year = {2005} }