{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T21:22:53Z","timestamp":1776115373665,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_11","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"131-146","source":"Crossref","is-referenced-by-count":140,"title":["Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"11_CR1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P.B. Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A theorem-proving system for classical type theory. J. Auto. Reas.\u00a016(3), 321\u2013353 (1996)","journal-title":"J. Auto. Reas."},{"issue":"8","key":"11_CR2","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/258949.258953","volume":"32","author":"J.M. Bell","year":"1997","unstructured":"Bell, J.M., Bellegarde, F., Hook, J.: Type-driven defunctionalization. ACM SIGPLAN Notices\u00a032(8), 25\u201337 (1997)","journal-title":"ACM SIGPLAN Notices"},{"key":"11_CR3","unstructured":"Benzm\u00fcller, C., Paulson, L., Theiss, F., Fietzke, A.: Progress report on LEO-II, an automatic theorem prover for higher-order logic. In: Schneider, K., Brandt, J. (eds.) TPHOLs: Emerging Trends. C.S. Dept., University of Kaiserslautern, Internal Report 364\/07 (2007)"},{"key":"11_CR4","first-page":"230","volume-title":"SEFM 2004","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Cuellar, J., Liu, Z. (eds.) SEFM 2004, pp. 230\u2013239. IEEE C.S., Los Alamitos (2004)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"IJCAR 2010","author":"J.C. Blanchette","year":"2010","unstructured":"Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, Springer, Heidelberg (to appear, 2010)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-540-74591-4_5","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Bulwahn","year":"2007","unstructured":"Bulwahn, L., Krauss, A., Nipkow, T.: Finding lexicographic orders for termination proofs in Isabelle\/HOL. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 38\u201353. Springer, Heidelberg (2007)"},{"key":"11_CR8","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: MODEL (2003)"},{"key":"11_CR9","unstructured":"de Medeiros Santos, A.L.: Compilation by Transformation in Non-Strict Functional Languages. Ph.D. thesis, C.S. Dept., University of Glasgow (1995)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-79124-9_8","volume-title":"Tests and Proofs","author":"A. Dunets","year":"2008","unstructured":"Dunets, A., Schellhorn, G., Reif, W.: Bounded relational analysis of free datatypes. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 99\u2013115. Springer, Heidelberg (2008)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-540-71209-1_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.F. Frias","year":"2007","unstructured":"Frias, M.F., Pombo, C.G.L., Moscato, M.M.: Alloy Analyzer + PVS in the analysis and verification of Alloy specifications. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 587\u2013601. Springer, Heidelberg (2007)"},{"key":"11_CR12","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"11_CR13","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Jackson, D.: Relational analysis of algebraic datatypes. In: Gall, H.C. (ed.) ESEC\/FSE 2005 (2005)","DOI":"10.1145\/1081706.1081740"},{"key":"11_CR15","unstructured":"McCune, W.: A Davis\u2013Putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical report, ANL (1994)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11921240_1","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"T. Nipkow","year":"2006","unstructured":"Nipkow, T.: Verifying a hotel key card system. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 1\u201314. Springer, Heidelberg (2006)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"11_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-22646-9","volume-title":"Automated Theorem Proving in Software Engineering","author":"J.M. Schumann","year":"2001","unstructured":"Schumann, J.M.: Automated Theorem Proving in Software Engineering. Springer, Heidelberg (2001)"},{"key":"11_CR19","unstructured":"Snelting, G., Wasserrab, D.: A correctness proof for the Volpano\/Smith security typing system. In: Klein, G., Nipkow, T., Paulson, L.C. (eds.) AFP (September 2008)"},{"key":"11_CR20","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library for automated theorem proving, \n                    \n                      http:\/\/www.cs.miami.edu\/~tptp\/"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"issue":"3","key":"11_CR22","first-page":"167","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Comp. Sec.\u00a04(3), 167\u2013187 (1996)","journal-title":"J. Comp. Sec."},{"key":"11_CR23","unstructured":"Weber, T.: SAT-Based Finite Model Generation for Higher-Order Logic. Ph.D. thesis, Dept. of Informatics, T.U. M\u00fcnchen (2008)"},{"key":"11_CR24","unstructured":"Zhang, J., Zhang, H.: SEM: A system for enumerating models. In: Kaufmann, M. (ed.) IJCAI 95, vol.\u00a01, pp. 298\u2013303 (1995)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:19Z","timestamp":1619785039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}