{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:21Z","timestamp":1776333381852,"version":"3.51.2"},"publisher-location":"Cham","reference-count":7,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319325811","type":"print"},{"value":"9783319325828","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-319-32582-8_14","type":"book-chapter","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T10:04:23Z","timestamp":1460023463000},"page":"208-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration"],"prefix":"10.1007","author":[{"given":"Jan","family":"Mr\u00e1zek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Bauch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrich","family":"Lauko","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,8]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-642-24372-1_3","volume-title":"Automated Technology for Verification and Analysis","author":"J Alglave","year":"2011","unstructured":"Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M.: Making software verification tools really work. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 28\u201342. Springer, Heidelberg (2011)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Barnat, J., Bauch, P., Havel, V.: Model checking parallel programs with inputs. In: 2014 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pp. 756\u2013759 (2014)","DOI":"10.1109\/PDP.2014.44"},{"key":"14_CR3","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 (CAV 2013)","author":"J Barnat","year":"2013","unstructured":"Barnat, J., et al.: DiVinE 3.0 \u2013 An explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification (CAV 2013). LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/978-3-319-14896-0_5","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"P Bauch","year":"2014","unstructured":"Bauch, P., Havel, V., Barnat, J.: LTL model checking of LLVM bitcode with symbolic data. 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. 47\u201359. Springer, Heidelberg (2014)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015)"},{"key":"14_CR6","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"14_CR7","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)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-32582-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:18:29Z","timestamp":1585012709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-32582-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319325811","9783319325828"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-32582-8_14","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":"8 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"}]}}