HOL-TestGen: An Interactive Test-case Generation Framework

By Achim D. Brucker and Burkhart Wolff.

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.

Further Reading:
This presentation is based on the following publication:
A. D. Brucker and B. Wolff, “HOL-TestGen: An interactive test-case generation framework,” in Fundamental approaches to software engineering (FASE09), M. Chechik and M. Wirsing, Eds. Heidelberg: Springer-Verlag, 2009, pp. 417–420. doi: 10.1007/978-3-642-00593-0_28. Author copy: http://logicalhacking.com/publications/brucker.ea-hol-testgen-2009/

Please cite this work as follows:
A. D. Brucker and B. Wolff, “HOL-TestGen: An interactive test-case generation framework,” presented at the Fundamental approaches to software engineering (FASE09), York, UK, Mar. 27, 2009. Author copy: http://logicalhacking.com/publications/talk-brucker.ea-hol-testgen-2009/

BibTeX
@Unpublished{ talk:brucker.ea:hol-testgen:2009,
  date       = {2009-03-27},
  title      = {HOL-TestGen: An Interactive Test-case Generation Framework},
  month      = {mar},
  language   = {USenglish},
  year       = {2009},
  venue      = {York, UK},
  author     = {Achim D. Brucker and Burkhart Wolff},
  eventtitle = {Fundamental Approaches to Software Engineering {(FASE09)}},
  areas      = {formal methods, software},
  abstract   = {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.},
  note       = {Author copy: \url{http://logicalhacking.com/publications/talk-brucker.ea-hol-testgen-2009/}},
}