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.