**Theorem-prover based testing** combines *testing and verification:*
tests are derived from a formal specification (or *model*, i.e., it
is a **model-based testing** technique) proof techniques.
**HOL-TestGen** is a
*theorem-prover based testing* environment on top of
Isabelle.

The main result of our work in the area of *theorem-prover based
testing* [1] is the
**HOL-TestGen** [2] system. HOL-TestGen is
jointly developed by the
Software Assurance & Security Research Team
at the University of Exeter, UK and the
Verified Algorithms, Languages and Systems
team at the LRI (CNRS and University of Paris-Sud), France.

As a unique feature, HOL-TestGen supports the end-to-end life-cycle of formal system testing and verification: from a formal specification that can be formally verified, to formally verified specification transformation (model-transformation), to abstract test case generation, concrete test data generation, to the generation and execution of test scrips that test a real system under test.

HOL-TestGen has been used in large case studies in various application domains,
including **conformance testing** of **security properties** (e.g., firewall
policies [3] and health-care-specific access
control systems [4]).

HOL-TestGen is free software; you can redistribute it and/or modify it under the terms of a BSD-style license.

[1]

A. D. Brucker and B. Wolff, “On theorem prover-based testing,” *Formal Aspects of Computing (FAC)*, vol. 25, no. 5, pp. 683–721, 2013, doi: 10.1007/s00165-012-0222-y.

[2]

A. D. Brucker and B. Wolff, “HOL-TestGen: An interactive test-case generation framework,” in *Fundamental approaches to software engineering (FASE09)*, M. Chechik and M. Wirsing, Eds. Heidelberg: Springer-Verlag, 2009, pp. 417–420. doi: 10.1007/978-3-642-00593-0_28.

[3]

A. D. Brucker, L. Brügger, and B. Wolff, “Formal firewall conformance testing: An application of test and proof techniques,” *Software Testing, Verification & Reliability (STVR)*, vol. 25, no. 1, pp. 34–71, 2015, doi: 10.1002/stvr.1544.

[4]

A. D. Brucker, L. Brügger, P. Kearney, and B. Wolff, “An approach to modular and testable security models of real-world health-care applications,” in *ACM symposium on access control models and technologies (SACMAT)*, 2011, pp. 133–142. doi: 10.1145/1998441.1998461.

[5]

A. D. Brucker, L. Brügger, and B. Wolff, “HOL-TestGen/FW: An environment for specification-based firewall conformance testing,” in *International colloquium on theoretical aspects of computing (ICTAC)*, Z. Liu, J. Woodcock, and H. Zhu, Eds. Heidelberg: Springer-Verlag, 2013, pp. 112–121. doi: 10.1007/978-3-642-39718-9_7.