@InCollection{	  brucker.ea:symbolic:2005,
  abstract	= {We present a method for the automatic generation of test
		  cases for HOL formulae containing primitive recursive
		  predicates. These test cases can be used for the animation
		  of specifications as well as for black-box testing of
		  external programs. Our method is two-staged: first, the
		  original formula is partitioned into test cases by
		  transformation into a Horn-clause normal form (HCNF).
		  Second, the test cases are analyzed for instances with
		  constant terms satisfying the premises of the clauses.
		  Particular emphasis is put on the control of test
		  hypotheses and test hierarchies to avoid intractability. We
		  applied our method to several examples, including AVL-trees
		  and the red-black tree implementation in the standard
		  library from SML/NJ. },
  keywords	= {symbolic test case generations, black box testing, theorem
		  proving, Isabelle/HOL },
  location	= {Linz},
  author	= {Achim D. Brucker and Burkhart Wolff},
  booktitle	= {Formal Approaches to Testing of Software},
  language	= {USenglish},
  pages		= {16--32},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  series	= {Lecture Notes in Computer Science},
  number	= {3395},
  isbn		= {3-540-25109-X},
  doi		= {10.1007/b106767},
  editor	= {Jens Grabowski and Brian Nielsen},
  pdf		= {http://www.brucker.ch/bibliography/download/2005/brucker.ea-symbolic-2005.pdf},
  project	= {CSFMDOS},
  title		= {Symbolic Test Case Generation for Primitive Recursive
		  Functions},
  classification= {workshop},
  areas		= {formal methods, software},
  categories	= {holtestgen},
  year		= {2004},
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-symbolic-2005}
		  
}