@InCollection{	  brucker.ea:interactive:2005,
  keywords	= {symbolic test case generations, black box testing, white
		  box testing, theorem proving, interactive testing},
  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. },
  location	= {Edinburgh},
  author	= {Achim D. Brucker and Burkhart Wolff},
  booktitle	= {Formal Approaches to Testing of Software},
  language	= {USenglish},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  series	= {Lecture Notes in Computer Science},
  number	= {3997},
  doi		= {10.1007/11759744_7},
  isbn		= {3-540-25109-X},
  editor	= {Wolfgang Grieskamp and Carsten Weise},
  pdf		= {http://www.brucker.ch/bibliography/download/2005/brucker.ea-interactive-2005.pdf},
  project	= {CSFMDOS},
  title		= {Interactive Testing using {HOL}-{TestGen}},
  classification= {workshop},
  areas		= {formal methods, software},
  categories	= {holtestgen},
  year		= {2005},
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-interactive-2005}
		  
}