%0 Book Section
%T HOL-TestGen: An Interactive Test-case Generation Framework
%A Brucker, Achim D.
%A Wolff, Burkhart
%E Chechik, Marsha
%E Wirsing, Martin
%B Fundamental Approaches to Software Engineering (FASE09)
%D 2009
%N 5503
%I Springer-Verlag
%C Heidelberg
%G USenglish
%F brucker.ea:hol-testgen:2009
%X We present HOL-TestGen, an extensible test environment for specification-based testing build upon the proof assistant Isabelle. HOL-TestGen leverages the semi-automated generation of test theorems (a form of a partition), and their refinement to concrete test data, as well as the automatic generation of a test driver for the execution and test result verification. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit and sequence test techniques in a logically consistent way. 
%K symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
%U http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009
%U http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.pdf
%U http://dx.doi.org/10.1007/978-3-642-00593-0_28
%P 417-420