{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T22:12:52Z","timestamp":1768255972268,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642380877","type":"print"},{"value":"9783642380884","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38088-4_1","type":"book-chapter","created":{"date-parts":[[2013,5,9]],"date-time":"2013-05-09T00:38:27Z","timestamp":1368059907000},"page":"1-15","source":"Crossref","is-referenced-by-count":12,"title":["Improved State Space Reductions for LTL Model Checking of C and C++ Programs"],"prefix":"10.1007","author":[{"given":"Petr","family":"Ro\u010dkai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 35\u201342. IEEE (2010)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-28891-3_25","volume-title":"NASA Formal Methods","author":"J. Barnat","year":"2012","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 252\u2013266. Springer, Heidelberg (2012)"},{"key":"1_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 2010), pp. 4\u20137. IEEE (2010)","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"key":"1_CR4","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"issue":"4","key":"1_CR6","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. Int. J. Found. Comput. Sci.\u00a014(4), 583\u2013604 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: International Conference on Software Engineering (ICSE 2000), pp. 439\u2013448. ACM (2000)","DOI":"10.1145\/337180.337234"},{"issue":"1","key":"1_CR9","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1047659.1040315","volume":"40","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. SIGPLAN Not.\u00a040(1), 110\u2013121 (2005)","journal-title":"SIGPLAN Not."},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: The verisoft approach. Formal Methods in System Design\u00a026(2), 77\u2013101 (2005)","journal-title":"Formal Methods in System Design"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.H.: A practical method for verifying event-driven software. In: International Conference on Software Engineering (ICSE 1999), pp. 597\u2013607. ACM (1999)","DOI":"10.1145\/302405.302710"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Iosif, R.: Exploiting Heap Symmetries in Explicit-State Model Checking of Software. In: 16th IEEE International Conference on Automated Software Engineering (ASE 2001), pp. 254\u2013261. IEEE Computer Society (2001)","DOI":"10.1109\/ASE.2001.989811"},{"key":"1_CR13","unstructured":"Norris Ip, C., Dill, D.L.: Efficient Verification of Symmetric Concurrent Systems. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 230\u2013234. IEEE Computer Society (1993)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software Verification Platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Path slicing. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2005), pp. 38\u201347. ACM Press (2005)","DOI":"10.1145\/1065010.1065016"},{"key":"1_CR16","unstructured":"Jones, R., Lins, R.D.: Garbage Collection: Algorithms for Automatic Dynamic Memory Management. Wiley (1996)"},{"key":"1_CR17","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 (Marh 2004)"},{"key":"1_CR18","unstructured":"http:\/\/www.llvm.org\/ (December 2012)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F. Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 146\u2013161. Springer, Heidelberg (2012)"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from One, One for All: on Model Checking Using Representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded Model Checking of Concurrent Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"issue":"4","key":"1_CR22","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1145\/1011508.1011511","volume":"26","author":"A. Prasad Sistla","year":"2004","unstructured":"Prasad Sistla, A., Godefroid, P.: Symmetry and reduced symmetry in model checking. ACM Trans. Program. Lang. Syst.\u00a026(4), 702\u2013734 (2004)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR23","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":"1_CR24","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"}],"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-38088-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:17:39Z","timestamp":1746004659000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38088-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642380877","9783642380884"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38088-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}