Back to the list of tutorials.
Theorem-Prover Based Testing with HOL-TestGen
Burkhart Wolff and Achim D. Brucker, ETH Zürich, Switzerland
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.