{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T01:18:44Z","timestamp":1725671924609},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_25","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"252-266","source":"Crossref","is-referenced-by-count":7,"title":["Towards LTL Model Checking of Unmodified Thread-Based C &amp; C++ Programs"],"prefix":"10.1007","author":[{"given":"Ji\u0159i","family":"Barnat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-540-27813-9_42","volume-title":"Computer Aided Verification","author":"T. Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A Model Checker for Concurrent Software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 484\u2013487. Springer, Heidelberg (2004)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume-title":"Integrated Formal Methods","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Ro\u010dkai, P.: DiVinE: Parallel Distributed Model Checker (Tool paper). In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi\/PDMC), pp. 4\u20137. IEEE (2010)","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Bingham, B., Bingham, J., de Paula, F.M., Erickson, J., Singh, G., Reitblatt, M.: Industrial Strength Distributed Explicit State Model Checking. In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi\/PDMC), pp. 28\u201336. IEEE (2010)","DOI":"10.1109\/PDMC-HiBi.2010.13"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A.: Modular verification of software components in C. IEEE Transactions on Software Engineering, 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: International Conference on Software Engineering, p. 439 (2000)","DOI":"10.1145\/337180.337234"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-00768-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N.H.M. Aan de Brugh","year":"2009","unstructured":"Aan de Brugh, N.H.M., Nguyen, V.Y., Ruys, T.C.: MoonWalker: Verification of.NET Programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 170\u2013173. Springer, Heidelberg (2009)"},{"issue":"7","key":"25_CR8","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. DeMartini","year":"1999","unstructured":"DeMartini, C., Iosif, R., Sisto, R.: A Deadlock Detection Tool for Concurrent Java Programs. Software Practice and Experience\u00a029(7), 577\u2013603 (1999)","journal-title":"Software Practice and Experience"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/10722468_8","volume-title":"SPIN Model Checking and Software Verification","author":"G.J. Holzmann","year":"2000","unstructured":"Holzmann, G.J.: Logic Verification of ANSI-C Code with SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 131\u2013147. Springer, Heidelberg (2000)"},{"key":"25_CR11","unstructured":"Holzmann, G.J.: The SPIN model checker: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)"},{"issue":"2","key":"25_CR12","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1002\/stvr.228","volume":"11","author":"G.J. Holzmann","year":"2001","unstructured":"Holzmann, G.J., Smith, M.H.: Software Model Checking: Extracting Verification Models from Source Code. Software Testing, Verification and Reliability\u00a011(2), 65\u201379 (2001)","journal-title":"Software Testing, Verification and Reliability"},{"key":"25_CR13","unstructured":"Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: International Symposium on Code Generation and Optimization (CGO), Palo Alto, California (March 2004)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-16164-3_16","volume-title":"Model Checking Software","author":"A. Linden","year":"2010","unstructured":"Linden, A., Wolper, P.: An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol.\u00a06349, pp. 212\u2013226. Springer, Heidelberg (2010)"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Musuvathi, M.S., Park, D., Chou, A., Engler, D.R., Dill, D.L.: CMC: A Pragmatic Approach to Model Checking Real Code. In: The Fifth Symposium on Operating Systems Design and Implementation (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1998","unstructured":"Peled, D.: Ten Years of Partial Order Reduction. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 17\u201328. Springer, Heidelberg (1998)"},{"key":"25_CR17","unstructured":"Brat, G., Thompson, S., Schimpf, K.: The MCP Model Checker (2008), Submitted to PEPM 2008"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Thompson, S., Brat, G.: Verification of C++ Flight Software with the MCP Model Checker. In: 2008 IEEE Aerospace Conference, pp. 1\u20139 (March 2008)","DOI":"10.1109\/AERO.2008.4526577"},{"key":"25_CR19","unstructured":"Thompson, S., Brat, G., Venet, A.: Software model checking of ARINC-653 flight code with MCP. In: Mu\u00f1oz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA\/CP-2010-216215, Langley Research Center, Hampton VA 23681-2199, USA, pp. 171\u2013181. NASA (April 2010)"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S.: Model Checking Programs. In: ASE, pp. 3\u201312 (2000)","DOI":"10.1109\/ASE.2000.873645"},{"issue":"1","key":"25_CR21","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/B:FORM.0000033963.55470.9e","volume":"25","author":"K. Yorav","year":"2004","unstructured":"Yorav, K., Grumberg, O.: Static Analysis for State-Space Reductions Preserving Temporal Logics. Formal Methods in System Design\u00a025(1), 67\u201396 (2004)","journal-title":"Formal Methods in System Design"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-85114-1_22","volume-title":"Model Checking Software","author":"A. Zaks","year":"2008","unstructured":"Zaks, A., Joshi, R.: Verifying Multi-threaded C Programs with SPIN. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 325\u2013342. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:18Z","timestamp":1620126858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}