{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:13:41Z","timestamp":1743153221374,"version":"3.40.3"},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319229683"},{"type":"electronic","value":"9783319229690"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22969-0_19","type":"book-chapter","created":{"date-parts":[[2015,8,20]],"date-time":"2015-08-20T08:51:42Z","timestamp":1440060702000},"page":"268-282","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Techniques for Memory-Efficient Model Checking of C and C++ Code"],"prefix":"10.1007","author":[{"given":"Petr","family":"Ro\u010dkai","sequence":"first","affiliation":[]},{"given":"Vladim\u00edr","family":"\u0160till","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,21]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J Barnat","year":"2013","unstructured":"Barnat, J., et al.: DiVinE 3.0 \u2013 an explicit-state model checker for multithreaded C and C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"issue":"1","key":"19_CR2","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.entcs.2007.10.018","volume":"198","author":"S Blom","year":"2008","unstructured":"Blom, S., Lisser, B., van de Pol, J., Weber, M.: A database approach to distributed state space generation. Electron. Notes Theor. Comput. Sci. 198(1), 17\u201332 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/3-540-48234-2_2","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"J Geldenhuys","year":"1999","unstructured":"Geldenhuys, J., de Villiers, P.J.A., Rushby, J.: Runtime efficient state compaction in SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 12\u201321. Springer, Heidelberg (1999)"},{"key":"19_CR4","unstructured":"Holzmann, G.J.: State compression in SPIN: recursive indexing and compression training runs. In: The International SPIN Workshop (1997)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Godefroid, P., Pirottin, D.: Coverage preserving reduction strategies for reachability analysis. In: PSTV, pp. 349\u2013363 (1992)","DOI":"10.1016\/B978-0-444-89874-6.50028-3"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-22306-8_4","volume-title":"Model Checking Software","author":"A Laarman","year":"2011","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) SPIN Workshops 2011. LNCS, vol. 6823, pp. 38\u201356. Springer, Heidelberg (2011)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"Computer Aided Verification","author":"D Peled","year":"1998","unstructured":"Peled, D.: Ten years of partial order reduction. In: Vardi, Moshe Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 17\u201328. Springer, Heidelberg (1998)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-38088-4_1","volume-title":"NASA Formal Methods","author":"P Ro\u010dkai","year":"2013","unstructured":"Ro\u010dkai, P., Barnat, J., Brim, L.: Improved state space reductions for LTL model checking of C and C++ programs. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 1\u201315. Springer, Heidelberg (2013)"},{"key":"19_CR9","unstructured":"\u0160till, V.: Compression, State Space, for the DiVinE Model Checker, : Bachelor\u2019s thesis. Masaryk University Brno, Faculty of Informatics (2013)"},{"issue":"3","key":"19_CR10","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1109\/TIT.1977.1055714","volume":"23","author":"J Ziv","year":"1977","unstructured":"Ziv, J., Lempel, A.: A universal algorithm for sequential data compression. IEEE Trans. Inf. Theor. 23(3), 337\u2013343 (1977)","journal-title":"IEEE Trans. Inf. Theor."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22969-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T14:45:01Z","timestamp":1676472301000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22969-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319229683","9783319229690"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22969-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"21 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}