Tutorial: Theorem-prover based Testing with HOL-TestGen

By Achim D. Brucker and Burkhart Wolff.

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.

Supplementary material:
[  Examples  ]

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Tutorial: Theorem-prover based testing with HOL-TestGen,” presented at the Testcom/fates 2007, Tallinn, Estonia, Jun. 26, 2007. Author copy: http://logicalhacking.com/publications/talk-brucker.ea-theorem-prover-2007/

BibTeX
@Unpublished{ talk:brucker.ea:theorem-prover:2007,
  date            = {2007-06-26},
  title           = {Tutorial: Theorem-prover based Testing with HOL-TestGen},
  author          = {Achim D. Brucker and Burkhart Wolff},
  lecturer        = {Achim D. Brucker and Burkhart Wolff},
  day             = {26},
  eventtitle      = {Testcom/Fates 2007},
  venue           = {Tallinn, Estonia},
  abstract        = {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.},
  supplementary01 = {/publications/talk-brucker.ea-theorem-prover-2007/talk-brucker.ea-theorem-prover-2007.tar.gz},
  supplabel01     = {Examples},
  note            = {Author copy: \url{http://logicalhacking.com/publications/talk-brucker.ea-theorem-prover-2007/}},
}