@Article{	  brucker.ea:theorem-prover:2012,
  author	= {Achim D. Brucker and Burkhart Wolff},
  journal	= {Formal Aspects of Computing},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  language	= {USenglish},
  categories	= {holtestgen},
  title		= {On Theorem Prover-based Testing},
  year		= {2012},
  issn		= {0934-5043},
  classification= journal,
  areas		= {formal methods, software},
  public	= {yes},
  doi		= {10.1007/s00165-012-0222-y},
  keywords	= {test case generation, domain partitioning, test sequence,
		  theorem proving, HOL-TestGen},
  abstract	= {HOL-TestGen is a specification and test case generation
		  environment extending the interactive theorem prover
		  Isabelle/HOL. As such, HOL-TestGen allows for an integrated
		  workflow supporting interactive theorem proving, test case
		  generation, and test data generation.
		  
		  The HOL-TestGen method is two-staged: first, the original
		  formula is partitioned into test cases by transformation
		  into a normal form called test theorem. Second, the test
		  cases are analyzed for ground instances (the 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.
		  
		  Due to the generality of the underlying framework, our
		  system can be used for black-box unit, sequence, reactive
		  sequence and white-box test scenarios. Although based on
		  particularly clean theoretical foundations, the system can
		  be applied for substantial case-studies. },
  pdf		= {http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012}
		  
}