@Article{	  brucker.ea:verifying:2008,
  abstract	= {HOL-TestGen is a specification and test case generation
		  environment extending the interactive theorem prover
		  Isabelle/\acs{hol}. The HOL-TestGen method is two-staged:
		  first, the original formula, called \emph{test
		  specification}, is partitioned into \emph{test cases} by
		  transformation into a normal form called \emph{test
		  theorem}. Second, the test cases are analyzed for ground
		  instances (the \emph{test data}) satisfying the constraints
		  of the test cases. Particular emphasis is put on the
		  control of explicit test hypotheses which can be proven
		  over concrete programs.
		  
		  As such, explicit test hypotheses establish a logical link
		  between validation by test and by proof. Since HOL-TestGen
		  generates explicit test hypotheses and makes them amenable
		  to formal proof, the system is in a unique position to
		  explore the relations between them at an example.},
  keywords	= {symbolic test case generations, black box testing, theorem
		  proving, formal verification, Isabelle/HOL},
  location	= {Budapest, Hungary},
  author	= {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  journal	= {Electronic Notes in Theoretical Computer Science},
  volume	= {220},
  number	= {1},
  issn		= {1571-0661},
  note		= {Proceedings of the Fourth Workshop on Model Based Testing
		  (MBT 2008)},
  publisher	= {Elsevier Science Publishers},
  address	= {Amsterdam},
  language	= {USenglish},
  editor	= {Bernd Finkbeiner and Yuri Gurevich and Alexander K.
		  Petrenko},
  title		= {Verifying Test-Hypotheses: An Experiment in Test and
		  Proof},
  categories	= {holtestgen},
  pages		= {15--27},
  classification= {workshop},
  areas		= {formal methods, software},
  year		= {2008},
  pdf		= {http://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.pdf},
  public	= {yes},
  doi		= {10.1016/j.entcs.2008.11.003},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-verifying-2008}
		  
}