{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:56Z","timestamp":1763468156837},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_60","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"863-868","source":"Crossref","is-referenced-by-count":62,"title":["DiVinE 3.0 \u2013 An Explicit-State Model Checker for Multithreaded C &amp; C++ Programs"],"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":"Vojt\u011bch","family":"Havel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Havl\u00ed\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Kriho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milan","family":"Len\u010do","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"}]},{"given":"Ji\u0159\u00ed","family":"Weiser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"60_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-32469-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"J. Barnat","year":"2012","unstructured":"Barnat, J., Beran, J., Brim, L., Kratochv\u00edla, T., Ro\u010dkai, P.: Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol.\u00a07437, pp. 78\u201392. Springer, Heidelberg (2012)"},{"key":"60_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-540-88387-6_20","volume-title":"Automated Technology for Verification and Analysis","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: DiVinE Multi-Core \u2013 A Parallel LTL Model-Checker. In: Cha, S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 234\u2013239. Springer, Heidelberg (2008)"},{"key":"60_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/11804192_13","volume-title":"Formal Methods for Components and Objects","author":"J. Barnat","year":"2006","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: Cluster-based LTL model checking of large systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 259\u2013279. Springer, Heidelberg (2006)"},{"key":"60_CR4","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. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 278\u2013281. Springer, Heidelberg (2006)"},{"key":"60_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-540-88387-6_20","volume-title":"Automated Technology for Verification and Analysis","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: DiVinE multi-core \u2013 A parallel LTL model-checker. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 234\u2013239. Springer, Heidelberg (2008)"},{"key":"60_CR6","doi-asserted-by":"crossref","unstructured":"Barnat, J., Havl\u00ed\u010dek, J., Ro\u010dkai, P.: Distributed LTL Model Checking with Hash Compaction. In: Proceedings of PASM\/PDMC 2012 (to appear 2013)","DOI":"10.1016\/j.entcs.2013.07.006"},{"key":"60_CR7","unstructured":"Behrmann, G., David, A., Larsen, K.G., M\u00f6ller, O., Pettersson, P., Yi, W.: Uppaal - present and future. In: Proc. of 40th IEEE Conference on Decision and Control. IEEE Computer Society Press (2001)"},{"key":"60_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/10722167_19","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2000","unstructured":"Behrmann, G., Hune, T., Vaandrager, F.W.: Distributing Timed Model Checking - How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 216\u2013231. Springer, Heidelberg (2000)"},{"key":"60_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/978-3-642-20398-5_40","volume-title":"NASA Formal Methods","author":"A. Laarman","year":"2011","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Multi-Core LTSmin: Marrying Modularity and Scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 506\u2013511. Springer, Heidelberg (2011)"},{"key":"60_CR10","doi-asserted-by":"crossref","unstructured":"Rockai, P., Barnat, J., Brim, L.: Improved State Space Reduction for LTL Model Checking of C & C++ Programs. In: Submitted to The 4th NASA Formal Methods Symposium (2013)","DOI":"10.1007\/978-3-642-38088-4_1"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_60","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:22:59Z","timestamp":1557930179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}