{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:33Z","timestamp":1779087633141,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540851134","type":"print"},{"value":"9783540851141","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85114-1_10","type":"book-chapter","created":{"date-parts":[[2008,8,13]],"date-time":"2008-08-13T03:22:48Z","timestamp":1218597768000},"page":"114-133","source":"Crossref","is-referenced-by-count":26,"title":["Efficient Modeling of Concurrent Systems in BMC"],"prefix":"10.1007","author":[{"given":"Malay K.","family":"Ganai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","volume-title":"Shared memory consistency models: A tutorial","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer, Los Alamitos (1996)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM (1978)","DOI":"10.1145\/359545.359563"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579. Springer, Heidelberg (1999)"},{"key":"10_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Ramalingam, G.: Context sensitive synchronization sensitive analysis is undecidable. In: ACM Transactions on Programming Languages and Systems (2000)","DOI":"10.1145\/349214.349241"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: Proc. of POPL (1997)","DOI":"10.1145\/263699.263717"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b98229","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.\u00a03170, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order Methods for the Verification of Concurrent Systems: An Approach to the State-explosion Problem. PhD thesis (1995)","DOI":"10.1007\/3-540-60761-7"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Transactions for software model checking. In: Proc. of TACAS (2003)","DOI":"10.1016\/S1571-0661(05)82560-5"},{"key":"10_CR10","unstructured":"Stoller, S.D.: Model-checking multi-threaded distributed Java programs. Journal on STTT (2002)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/3-540-36577-X_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S.D. Stoller","year":"2003","unstructured":"Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 489\u2013504. Springer, Heidelberg (2003)"},{"key":"10_CR12","unstructured":"Levin, V., Palmer, R., Qadeer, S., Rajamani, S.K.: Sound transaction-based reduction without cycle detection. In: Proc. of SPIN Workshop (2003)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Proc. of CAV, pp. 340\u2013351 (1997)","DOI":"10.1007\/3-540-63166-6_34"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: Proc. of CAV (2006)","DOI":"10.1007\/11817963_28"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Proc. of CAV (2005)","DOI":"10.1007\/11513988_9"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Lerda, F., Sinha, N., Theobald, M.: Symbolic model checking of software. Electronic Notes Theoretical Computer Science (2003)","DOI":"10.1016\/S1571-0661(05)80008-8"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided Underapproximation-Widening for Multi-process Sytems. In: Proc. of POPL (2005)","DOI":"10.1145\/1040305.1040316"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Symbolic Model Checking for Asynchronous Boolean Programs. In: Proc. of SPIN Workshop (2005)","DOI":"10.1007\/11537328_9"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: Proc. of ICCAD (2006)","DOI":"10.1109\/ICCAD.2006.320122"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Hill, M.D., Miller, B.P., Netzer, R.H.B.: Detecting data races on weak memory systems. In: Proc. of ISCA (1991)","DOI":"10.1145\/115952.115976"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/978-3-540-30482-1_11","volume-title":"Formal Methods and Software Engineering","author":"Y. Yang","year":"2004","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 30\u201345. Springer, Heidelberg (2004)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: Checking consistency of concurrent data types on relaxed memory models. In: Proc. of PLDI (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: Proc. of IPDPS (2004)","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Voung, J.W., Jhala, R., Lerner, S.: Relay: static race detection on millions of lines of code. In: ESEC\/SIGSOFT FSE, pp. 205\u2013214 (2007)","DOI":"10.1145\/1287624.1287654"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: Proc. of POPL, pp. 327\u2013338 (2007)","DOI":"10.1145\/1190216.1190265"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","volume-title":"Leveraging Applications of Formal Methods","author":"F. Ivan\u010di\u0107","year":"2006","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based Bounded Model Checking for Software Verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol.\u00a04313. Springer, Heidelberg (2006)"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Completeness in SMT-based BMC for software programs. In: Proc. of DATE (2008)","DOI":"10.1109\/DATE.2008.4484777"},{"key":"10_CR30","unstructured":"Joint CAV\/ISSTA\u00a0Special Event. Specification, Verification, and Testing of Concurrent Software (2004), http:\/\/research.microsoft.com\/~quadeer\/cav-issta.htm"},{"key":"10_CR31","unstructured":"SRI. Yices: An SMT solver, http:\/\/fm.csl.sri.com\/yices"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: Proc. of DAC (2003)","DOI":"10.21236\/ADA461052"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85114-1_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:22:04Z","timestamp":1606184524000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85114-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851134","9783540851141"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85114-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}