Download HOL-TestGen: User Guide

[19] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis
of programs by construction or approximation of fixpoints. In Proceedings of the the 4th ACM
SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238–252, New
York, ny usa, 1977. acm Press.
[20] O.-J. Dahl, E. W. Dijkstra, and C. A. R. Hoare. Structured Programming, volume 8 of A.P.I.C.
Studies in Data Processing. Academic Press, London, 3rd edition, 1972.
[21] J. Dick and A. Faivre. Automating the generation and sequencing of test cases from model-based
specications. In J. Woodcock and P. Larsen, editors, Formal Methods Europe 93: IndustrialStrength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 268–284,
Heidelberg, Apr. 1993. Springer-Verlag.
[22] P. Dybjer, Q. Haiyan, and M. Takeyama. Verifying haskell programs by combining testing and
proving. In Proceedings of the Third International Conference on Quality Software, page 272.
IEEE Computer Society, 2003.
[23] J. S. Fitzgerald, C. B. Jones, and P. Lucas, editors. volume 1313 of Lecture Notes in Computer
Science, Heidelberg, 1997. Springer-Verlag.
[24] M. C. Gaudel. Testing can be formal, too. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach,
editors, tapsoft’95: Theory and Practice of Software Development, number 915 in Lecture
Notes in Computer Science, pages 82–96. Springer-Verlag, Heidelberg, 1995.
[25] S. Hayashi. Towards the animation of proofs—testing proofs by examples. Theoretical Computer
Science, 272(1–2):177–195, 2002.
[26] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/ hol—A Proof Assistant for Higher-Order
Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2002.
[27] N. D. North. Automatic test generation for the triangle problem. Technical Report DITC
161/90, National Physical Laboratory, Teddington, Middlesex TW11 0LW, UK, Feb. 1990.
[28] A. Roscoe. Theory and Practice of Concurrency. Prentice Hall, 1998.
[29] H. Tej and B. Wolff. A corrected failure divergence model for CSP in Isabelle/HOL. In Fitzgerald
et al. [23], pages 318–337.
[30] D. von Bidder. Specification-based Firewall Testing. Ph.d. thesis, ETH Zurich, 2007. eth
Dissertation No. 17172. Diana von Bidder’s maiden name is Diana Senn.
[31] M. Wenzel. The Isabelle/Isar Reference Manual. TU München, München, 2004.
[32] H. Zhu, P. A. Hall, and J. H. R. May. Software unit test coverage and adequacy. ACM Computing
Surveys, 29(4):366–427, Dec. 1997.
246