{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:17:55Z","timestamp":1775053075316,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540344544","type":"print"},{"value":"9783540344551","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11759744_7","type":"book-chapter","created":{"date-parts":[[2006,6,2]],"date-time":"2006-06-02T12:27:50Z","timestamp":1149251270000},"page":"87-102","source":"Crossref","is-referenced-by-count":9,"title":["Interactive Testing with HOL-TestGen"],"prefix":"10.1007","author":[{"given":"Achim D.","family":"Brucker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"HOL-TestGen, http:\/\/www.brucker.ch\/projects\/hol-testgen\/"},{"key":"7_CR2","unstructured":"IMP, http:\/\/isabelle.in.tum.de\/library\/HOL\/IMP\/Denotation.html"},{"key":"7_CR3","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"1986","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, Orlando (1986)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: Proceedings of the international symposium on Software testing and analysis, pp. 123\u2013133 (2002)","DOI":"10.1145\/566172.566191"},{"key":"7_CR5","unstructured":"Brucker, A.D., Wolff, B.: HOL-TestGen 1.0.0 user guide. Technical Report 482, ETH Z\u00fcrich (April 2005)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-31848-4_2","volume-title":"Formal Approaches to Software Testing","author":"A.D. Brucker","year":"2005","unstructured":"Brucker, A.D., Wolff, B.: Symbolic test case generation for primitive recursive functions. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol.\u00a03395, pp. 16\u201332. Springer, Heidelberg (2005)"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"issue":"15","key":"7_CR8","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.infsof.2004.07.007","volume":"46","author":"W. Grieskamp","year":"2004","unstructured":"Grieskamp, W., Tillmann, N., Veanes, M.: Instrumenting scenarios in a model-driven development environment. Information and Software Technology\u00a046(15), 1027\u20131036 (2004)","journal-title":"Information and Software Technology"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing\u00a010, 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"2","key":"7_CR11","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engg.\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engg."},{"key":"7_CR12","unstructured":"Wenzel, M.M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, TU M\u00fcnchen, M\u00fcnchen (February 2002)"},{"key":"7_CR13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Formal Approaches to Software Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11759744_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T06:28:41Z","timestamp":1586932121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11759744_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540344544","9783540344551"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11759744_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}