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 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, Lukas Brügger, Matthias Krieger, and Burkhart Wolff.

Download

hol-testgen-1.5.0-pre.tar.gz (ca. 1.9 MiB, MD5: 84409a44718ef6cd7e276ddeb33fa3b9, 2010-04-02) ChangeLog

Related Publications

2010

• Achim D. Brucker and Lukas Brügger and Matthias P. Krieger and Burkhart Wolff. HOL-TestGen 1.5.0 User Guide. ETH Zurich, Technical Report 670, 2010.
  Categories: ,
  (PDF) (BibTeX) (Endnote) (RIS) ( )
  
• Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. Verified Firewall Policy Transformations for Test-Case Generation. In Third International Conference on Software Testing, Verification, and Validation (ICST), pages 345-354, 2010.
  Categories: ,
  (abstract) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1109/ICST.2010.50) ( )
  

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) ( )