write test specifications in Higher-order logics (HOL)
(semi-) automatically partition the input space, resulting in abstract test cases
automatically select concrete test data
automatically generate test scripts (in SML)
using a foreign language interface, implementations in arbitrary languages (e.g. C) can be tested.
HOL-TestGen is free software; you can redistribute it and/or modify it under the terms of a BSD-style licence. It is developed by Achim D. Brucker and Burkhart Wolff.
HOL-TestGen has been deposited in the Agency for the protection of programs (APP) IDDN.FR.001.220032.000.S.A.2011.000.10000 (Signed Paris, 3.6. 2011)