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 partitioning the test input space), 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
test and sequence test techniques in a logically consistent way.
Keywords symbolic test-case generations - black box testing - white box testing - theorem proving - interactive testing