{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T00:57:35Z","timestamp":1768265855388,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":4,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_60","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"920-922","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["DIVINE: Explicit-State LTL Model Checker"],"prefix":"10.1007","author":[{"given":"Vladim\u00edr","family":"\u0160till","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"60_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 & C++. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"key":"60_CR2","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":"60_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-319-22969-0_19","volume-title":"Software Engineering and Formal Methods","author":"P Ro\u010dkai","year":"2015","unstructured":"Ro\u010dkai, P., \u0160till, V., Barnat, J.: Techniques for memory-efficient model checking of C and C++ code. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 268\u2013282. Springer, Heidelberg (2015)"},{"key":"60_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-319-14896-0_12","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"V \u0160till","year":"2014","unstructured":"\u0160till, V., Ro\u010dkai, P., Barnat, J.: Context-switch-directed verification in DIVINE. In: Hlin\u011bn\u00fd, P., Dvo\u0159\u00e1k, Z., Jaro\u0161, J., Kofro\u0148, J., Ko\u0159enek, J., Matula, P., Pala, K. (eds.) MEMICS 2014. LNCS, vol. 8934, pp. 135\u2013146. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_60","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:17:10Z","timestamp":1585012630000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_60"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":4,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}