{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:58:43Z","timestamp":1743062323104,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642032394"},{"type":"electronic","value":"9783642032400"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03240-0_14","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T10:27:38Z","timestamp":1248690458000},"page":"150-165","source":"Crossref","is-referenced-by-count":5,"title":["Can Flash Memory Help in Model Checking?"],"prefix":"10.1007","author":[{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damian","family":"Sulewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavel","family":"\u0160ime\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"9","key":"14_CR1","doi-asserted-by":"publisher","first-page":"1116","DOI":"10.1145\/48529.48535","volume":"31","author":"A. Aggarwal","year":"1988","unstructured":"Aggarwal, A., Vitter, J.S.: The input\/output complexity of sorting and related problems. Commun. ACM\u00a031(9), 1116\u20131127 (1988)","journal-title":"Commun. ACM"},{"key":"14_CR2","volume-title":"Algorithms for Memory Hierarchies","author":"P. Sanders","year":"2002","unstructured":"Sanders, P., Meyer, U., Sibeyn, J.F.: Algorithms for Memory Hierarchies. Springer, Heidelberg (2002)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-74309-5_9","volume-title":"Advances in Computer Systems Architecture","author":"S.L. Min","year":"2007","unstructured":"Min, S.L., Nam, E.H., Lee, Y.H.: Evolution of NAND flash memory interface. In: Choi, L., Paek, Y., Cho, S. (eds.) ACSAC 2007. LNCS, vol.\u00a04697, pp. 75\u201379. Springer, Heidelberg (2007)"},{"key":"14_CR4","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"unstructured":"Korf, R.: Best-First Frontier Search with Delayed Duplicate Detection. In: AAAI 2004, pp. 650\u2013657. AAAI Press \/ The MIT Press (2004)","key":"14_CR5"},{"unstructured":"Korf, R., Schultze, P.: Large-Scale Parallel Breadth-First Search. In: AAAI 2005, pp. 1380\u20131385. AAAI Press \/ The MIT Press (2005)","key":"14_CR6"},{"unstructured":"Munagala, K., Ranade, A.: I\/O-Complexity of Graph Algorithms. In: SODA 1999, Philadelphia, PA, USA, pp. 687\u2013694. Society for Industrial and Applied Mathematics (1999)","key":"14_CR7"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Stern, U., Dill, D.L.: Using Magnetic Disk Instead of Main Memory in the Murphi Verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-70952-7_4","volume-title":"Formal Methods: Applications and Technology","author":"M. Hammer","year":"2007","unstructured":"Hammer, M., Weber, M.: To Store Or Not To Store Reloaded: Reclaiming Memory On Demand. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 51\u201366. Springer, Heidelberg (2007)"},{"unstructured":"Barnat, J.: Distributed Memory LTL Model Checking. PhD thesis, Faculty of Informatics, Masaryk University Brno (2004)","key":"14_CR10"},{"issue":"2-3","key":"14_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des.\u00a01(2-3), 275\u2013288 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11691617_1","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Large-Scale Directed Model Checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-73368-3_32","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P.: I\/O Efficient Accepting Cycle Detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 281\u2013293. Springer, Heidelberg (2007)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-78800-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P., Weber, M.: Revisiting Resistance Speeds Up I\/O-Efficient LTL Model Checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 48\u201362. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci.\u00a066(2) (2002)","key":"14_CR15","DOI":"10.1016\/S1571-0661(04)80410-9"},{"issue":"2\u20133","key":"14_CR16","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-003-0121-x","volume":"5","author":"V. Schuppan","year":"2004","unstructured":"Schuppan, V., Biere, A.: Efficient Reduction of Finite State Model Checking to Reachability Analysis. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(2\u20133), 185\u2013204 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"unstructured":"Kim, K., Choi, J.H., Choi, J., Jeong, H.S.: The future prospect of nonvolatile memory. In: 2005 IEEE VLSI-TSA International Symposium on VLSI Technology (VLSI-TSA-Tech), pp. 88\u201394 (2005)","key":"14_CR17"},{"key":"14_CR18","volume-title":"The Art of Computer Programming: Sorting and Searching","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming: Sorting and Searching, vol.\u00a03. Addison Wesley, Reading (1973)"},{"issue":"7","key":"14_CR19","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"B. Bloom","year":"1970","unstructured":"Bloom, B.: Space\/time trade-offs in hashing coding with allowable errors. Communication of the ACM\u00a013(7), 422\u2013426 (1970)","journal-title":"Communication of the ACM"},{"issue":"3","key":"14_CR20","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/s100090050034","volume":"2","author":"G.J. Holzmann","year":"1999","unstructured":"Holzmann, G.J., Puri, A.: A minimized automaton representation of reachable states. International Journal on Software Tools for Technology Transfer\u00a02(3), 270\u2013278 (1999)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"3","key":"14_CR21","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System Design\u00a013(3), 287\u2013305 (1998)","journal-title":"Formal Methods in System Design"},{"unstructured":"Stern, U., Dill, D.L.: Combining state space caching and hash compaction. In: Methoden des Entwurfs und der Verifikation digitaler Systeme, 4. GI\/ITG\/GME Workshop, pp. 81\u201390. Shaker Verlag, Aachen (1996)","key":"14_CR22"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-73951-7_13","volume-title":"Algorithms and Data Structures","author":"F.C. Botelho","year":"2007","unstructured":"Botelho, F.C., Pagh, R., Ziviani, N.: Simple and space-efficient minimal perfect hash functions. In: Dehne, F., Sack, J.-R., Zeh, N. (eds.) WADS 2007. LNCS, vol.\u00a04619, pp. 139\u2013150. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Botelho, F.C., Ziviani, N.: External perfect hashing for very large key sets. In: CIKM 2007: Proceedings of the sixteenth ACM Conference on information and knowledge management, pp. 653\u2013662 (2007)","key":"14_CR24","DOI":"10.1145\/1321440.1321532"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-70545-1_50","volume-title":"Computer Aided Verification","author":"S. Edelkamp","year":"2008","unstructured":"Edelkamp, S., Sanders, P., Simecek, P.: Semi-external LTL model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 530\u2013542. Springer, Heidelberg (2008)"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44676-1_10","volume-title":"Algorithms - ESA 2001","author":"R. Pagh","year":"2001","unstructured":"Pagh, R., Rodler, F.F.: Cuckoo hashing. In: Meyer auf der Heide, F. (ed.) ESA 2001. LNCS, vol.\u00a02161, pp. 121\u2013133. Springer, Heidelberg (2001)"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11817963_26","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2006","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Moravec, P., Ro\u010dkai, P., \u0160ime\u010dek, P.: DiVinE \u2013 A Tool for Distributed Verification (Tool Paper). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 278\u2013281. Springer, Heidelberg (2006)"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Schwoon","year":"2005","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 174\u2013190. Springer, Heidelberg (2005)"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/11561071_57","volume-title":"Algorithms \u2013 ESA 2005","author":"R. Dementiev","year":"2005","unstructured":"Dementiev, R., Kettner, L., Sanders, P.: STXXL: Standard template library for XXL data sets. In: Brodal, G.S., Leonardi, S. (eds.) ESA 2005. LNCS, vol.\u00a03669, pp. 640\u2013651. Springer, Heidelberg (2005)"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03240-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:26:12Z","timestamp":1558268772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03240-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032394","9783642032400"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03240-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}