{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:16:32Z","timestamp":1743041792228,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319148953"},{"type":"electronic","value":"9783319148960"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-14896-0_12","type":"book-chapter","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T06:06:08Z","timestamp":1420005968000},"page":"135-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Context-Switch-Directed Verification in DIVINE"],"prefix":"10.1007","author":[{"given":"Vladim\u00edr","family":"\u0160till","sequence":"first","affiliation":[]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,1,1]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-28644-8_1","volume-title":"CONCUR 2004 - Concurrency Theory","author":"T Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-00768-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MF Atig","year":"2009","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 107\u2013123. Springer, Heidelberg (2009)"},{"key":"12_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","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.) CAV 2013. LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"issue":"12","key":"12_CR4","doi-asserted-by":"publisher","first-page":"1272","DOI":"10.1016\/j.scico.2011.03.001","volume":"77","author":"J Barnat","year":"2012","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming 77(12), 1272\u20131288 (2012)","journal-title":"Science of Computer Programming"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-73368-3_24","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2007","unstructured":"Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 207\u2013220. Springer, Heidelberg (2007)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-30494-4_25","volume-title":"Formal Methods in Computer-Aided Design","author":"L Brim","year":"2004","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: Accepting predecessors are better than back edges in distributed LTL model-checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 352\u2013366. Springer, Heidelberg (2004)"},{"key":"12_CR7","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: POPL, pp. 174\u2013186. ACM Press (1997)","DOI":"10.1145\/263699.263717"},{"key":"12_CR9","unstructured":"Holzmann, G.J.: The Spin Model Checker Primer and Reference Manual. Addison-Wesley (2004)"},{"issue":"3","key":"12_CR10","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/s00165-010-0160-5","volume":"23","author":"GJ Holzmann","year":"2011","unstructured":"Holzmann, G.J., Florian, M.: Model checking with bounded context switching. Formal Aspects of Computing 23(3), 365\u2013389 (2011)","journal-title":"Formal Aspects of Computing"},{"issue":"6","key":"12_CR11","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"GJ Holzmann","year":"2011","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Transactions on Software Engineering 37(6), 845\u2013857 (2011)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"12_CR12","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. 6617, pp. 506\u2013511. Springer, Heidelberg (2011)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: ACM SIGPLAN, PLDI, PLDI 2007, pp. 446\u2013455. ACM, New York (2007)","DOI":"10.1145\/1273442.1250785"},{"key":"12_CR14","unstructured":"Musuvathi, M., Qadeer, S.: Partial-Order Reduction for Context-Bounded State Exploration. Technical Report MSR-TR-2007-12, Microsoft Research (2007)"},{"issue":"6","key":"12_CR15","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/1379022.1375625","volume":"43","author":"M Musuvathi","year":"2008","unstructured":"Musuvathi, M., Qadeer, S.: Fair Stateless Model Checking. ACM SIGPLAN Notices 43(6), 362\u2013371 (2008)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Nagarakatte, S., Burckhardt, S., Martin, M.M.K., Musuvathi, M.: Multicore acceleration of priority-based schedulers for concurrency bug detection. In: ACM SIGPLAN, PLDI, pp. 543\u2013554. ACM (2012)","DOI":"10.1145\/2345156.2254128"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, Lenore D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"12_CR18","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","Mathematical and Engineering Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-14896-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T12:27:09Z","timestamp":1675254429000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-14896-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319148953","9783319148960"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-14896-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"1 January 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}