# Tutorial (2009):

## Theorem-prover Based Testing with HOL-TestGen

Many testing techniques vitally depend on symbolic computation and
constraint-solving techniques. Their limits therefore represent limits
for testing as a whole. The HOL-TestGen system is designed as plug-in
into the state-of-the-art theorem proving environment
Isabelle/HOL. Thus, powerful modeling languages as well as powerful
automated and interactive proof methods for constraint resolution are
available. HOL-TestGen has been applied in unit, sequence, and
reactive sequence black-box test scenarios in substantial case
studies. Conceptually, it offers a quite unique combined view on these
areas traditionally considered separately. Moreover, it bridges the
gap to traditional program verification by concepts such as 'explicit
test hypothesis'. The tutorial is going to be a guided tour through
theory, pragmatics, and case-studies.

(
slides)
(
handout)
(examples)