@InCollection{ brucker.ea:interactive:2005, abstract = {HOL-TestGen is a test environment for specification-based unit testing build upon the proof assistant Isabelle/HOL\@. While there is considerable skepticism with regard to interactive theorem provers in testing communities, we argue that they are a natural choice for (automated) symbolic computations underlying systematic tests. This holds in particular for the development on non-trivial formal test plans of complex software, where some parts of the overall activity require inherently guidance by a test engineer. In this paper, we present the underlying methods for both black box and white box testing in interactive unit test scenarios. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit test techniques in a logically consistent way. }, address = {Edinburgh}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Formal Approaches to Testing of Software (FATES 05)}, copyright = {\copyright Springer-Verlag}, copyrighturl = {http://dx.doi.org/10.1007/11759744_7}, editor = {Wolfgang Grieskamp and Carsten Weise}, isbn = {3-540-25109-X}, language = {USenglish}, pages = {87--102}, publisher = {Springer-Verlag}, series = {LNCS 3997}, title = {Interactive Testing using {HOL-TestGen}}, year = 2005, user = {wolff} }