HOL-TestGen

HOL-TestGen is a is a test case generator for specification based unit testing. HOL-TestGen is built on top of the specfication and theorem proving environment Isabelle/HOL.

hol-TestGen screenshot

HOL-TestGen allows one to

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

Download

hol-testgen-1.4.0.tar.gz (ca. 504 kByte, MD5: 5cc9c04b5e829fa729ec4c2a5fccb2fd, 2008-06-19) ChangeLog

Debian Packages

If you use the Debian GNU/Linux distribution, you can also install HOL-TestGen using the following apt-repository:

deb http://projects.brucker.ch/debian/rep unstable main
deb-src http://projects.brucker.ch/debian/rep unstable main

Note: replace unstable by the distribution you are using, e.g., stable, testing, or unstable.

Related Publications

2010

Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. Verified Firewall Policy Transformations for Test-Case Generation. In International Conference on Software Testing, Verification, and Validation (ICST), 2010.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) ( )

2009

Achim D. Brucker and Burkhart Wolff. HOL-TestGen: An Interactive Test-case Generation Framework. In Fundamental Approaches to Software Engineering (FASE09). Lecture Notes in Computer Science (5503), pages 417-420, Springer-Verlag , 2009.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-642-00593-0_28) ( )

2008

Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Verifying Test-Hypotheses: An Experiment in Test and Proof. In Electronic Notes in Theoretical Computer Science, 220 (1), pages 15-27, 2008. Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008)
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1016/j.entcs.2008.11.003) ( )
Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Model-based Firewall Conformance Testing. In Testcom/FATES 2008. Lecture Notes in Computer Science (5047), pages 103-118, Springer-Verlag , 2008.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-540-68524-1_9) ( )

2007

Achim D. Brucker and Burkhart Wolff. Test-Sequence Generation with HOL-TestGen - With an Application to Firewall Testing. In TAP 2007: Tests And Proofs. Lecture Notes in Computer Science (4454), pages 149-168, Springer-Verlag , 2007.
Categories: , ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-540-73770-4_9) ( )

2005

Achim D. Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 User Guide. ETH Zurich, Technical Report 482, 2005.
Categories: ,
(PDF) (BibTeX) (Endnote) (RIS) ( )
Achim D. Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Formal Approaches to Testing of Software. Lecture Notes in Computer Science (3997), Springer-Verlag , 2005.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/11759744_7) ( )

2004

Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. ETH Zurich, Technical Report 449, 2004.
(abstract) (PDF) (BibTeX) (Endnote) (RIS) ( )
Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Formal Approaches to Testing of Software. Lecture Notes in Computer Science (3395), pages 16-32, Springer-Verlag , 2004.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/b106767) ( )