@Article{ brucker.ea:verifying:2008,
abstract = {HOL-TestGen is a specification and test case generation
environment extending the interactive theorem prover
Isabelle/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 = j-entcs,
volume = {220},
number = {1},
issn = {1571-0661},
note = {Proceedings of the Fourth Workshop on Model Based Testing
(MBT 2008)},
publisher = pub-elsevier,
address = pub-elsevier:adr,
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 = {https://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.pdf},
public = {yes},
doi = {10.1016/j.entcs.2008.11.003},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-verifying-2008}
}