{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:33Z","timestamp":1776305373887,"version":"3.50.1"},"publisher-location":"Cham","reference-count":8,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319681665","type":"print"},{"value":"9783319681672","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_14","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"201-207","source":"Crossref","is-referenced-by-count":48,"title":["Model Checking of C and C++ with DIVINE 4"],"prefix":"10.1007","author":[{"given":"Zuzana","family":"Baranov\u00e1","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katar\u00edna","family":"Kejstov\u00e1","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tade\u00e1\u0161","family":"Ku\u010dera","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrich","family":"Lauko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Mr\u00e1zek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladim\u00edr","family":"\u0160till","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$ -automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). doi: 10.1007\/978-3-319-46520-3_8"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-319-32582-8_14","volume-title":"Model Checking Software","author":"J Mr\u00e1zek","year":"2016","unstructured":"Mr\u00e1zek, J., Bauch, P., Lauko, H., Barnat, J.: SymDIVINE: tool for control-explicit data-symbolic state space exploration. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 208\u2013213. Springer, Cham (2016). doi: 10.1007\/978-3-319-32582-8_14"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L., Fischer, B.: SMT-based bounded model checking of C++ programs. In: Engineering of Computer Based Systems (ECBS), pp. 147\u2013156. IEEE Computer Society (2013)","DOI":"10.1109\/ECBS.2013.15"},{"key":"14_CR4","unstructured":"Ro\u010dkai, P., Barnat, J.: A Simulator for LLVM Bitcode. Preliminary version, arXiv:1704.05551 (2017)"},{"key":"14_CR5","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 & C++ programs. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013, vol. 7871, pp. 1\u201315. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38088-4_1"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Ro\u010dkai, P., \u0160till, V., \u010cern\u00e1, I., Barnat, J.: DiVM: Model Checking with LLVM and Graph Memory. Preliminary version, arXiv:1703.05341 (2017)","DOI":"10.1016\/j.jss.2018.04.026"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-29817-7_13","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"V \u0160till","year":"2016","unstructured":"\u0160till, V., Ro\u010dkai, P., Barnat, J.: Weak memory models as LLVM-to-LLVM transformations. In: Kofro\u0148, J., Vojnar, T. (eds.) MEMICS 2015. LNCS, vol. 9548, pp. 144\u2013155. Springer, Cham (2016). doi: 10.1007\/978-3-319-29817-7_13"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"\u0160till, V., Ro\u010dkai, P., Barnat, J.: Using off-the-shelf exception support components in C++ verification. In: IEEE International Conference on Software Quality, Reliability and Security (QRS 2017) (2017). doi: 10.1109\/QRS.2017.15","DOI":"10.1109\/QRS.2017.15"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T19:37:56Z","timestamp":1570131476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}