{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:23Z","timestamp":1776304943366,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_9","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"141-157","source":"Crossref","is-referenced-by-count":100,"title":["Partial Orders for Efficient Bounded Model Checking of\u00a0Concurrent\u00a0Software"],"prefix":"10.1007","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Gharachorloo, K.: Shared Memory Consistency Models: A Tutorial. IEEE Computer (1995)","DOI":"10.21236\/ADA638015"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 512\u2013532. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient BMC of concurrent software. CoRR abs\/1301.1629 (2013)","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models (Extended Version). In: FMSD (2012)","DOI":"10.1007\/s10703-011-0135-z"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in the analysis of weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 99\u2013115. Springer, Heidelberg (2011)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Ben-Asher, Y., Farchi, E.: Using True Concurrency to Model Execution of Parallel Programs. In: IJPP (1994)","DOI":"10.1007\/BF02577738"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Second competition on software verification. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 594\u2013609. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 533\u2013553. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.: CheckFence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"9_CR11","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":"9_CR12","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)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: ICSE (2011)","DOI":"10.1145\/1985793.1985839"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. TCAD (2008)","DOI":"10.1109\/TCAD.2008.923410"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Fischer, B., Inverso, O., Parlato, G.: CSeq: A sequentialization tool for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 616\u2013618. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_46"},{"key":"9_CR16","volume-title":"SPIN","author":"M. Ganai","year":"2008","unstructured":"Ganai, M., Gupta, A.: Efficient modeling of concurrent systems in BMC. In: SPIN. Springer, Heidelberg (2008)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-27813-9_31","volume-title":"Computer Aided Verification","author":"G.C. Gopalakrishnan","year":"2004","unstructured":"Gopalakrishnan, G.C., Yang, Y., Sivaraj, H.: QB or not QB: An efficient execution verification tool for memory orderings. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 401\u2013413. Springer, Heidelberg (2004)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-22110-1_32","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 412\u2013417. Springer, Heidelberg (2011)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Huynh, Q., Roychoudhury, A.: A memory sensitive checker for C#. In: FM (2006)","DOI":"10.1007\/11813040_32"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: DAC (2003)","DOI":"10.21236\/ADA461052"},{"key":"9_CR22","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD (2010)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. In: FMSD (2009)","DOI":"10.1007\/s10703-009-0078-9"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. CACM (1978)","DOI":"10.1145\/359545.359563"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Lamport, L.: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput. (1979)","DOI":"10.1109\/TC.1979.1675439"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-31424-7_36","volume-title":"Computer Aided Verification","author":"S. Mador-Haim","year":"2012","unstructured":"Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M.M.K., Sewell, P., Williams, D.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 495\u2013512. Springer, Heidelberg (2012)"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"9_CR29","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":"9_CR30","doi-asserted-by":"crossref","unstructured":"Pratt, V.: Modeling Concurrency with Partial Orders. International Journal of Parallel Programming (1986)","DOI":"10.1007\/BF01379149"},{"key":"9_CR31","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, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding Power Multiprocessors. In: PLDI (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: Staged concurrent program analysis. In: FSE (2010)","DOI":"10.1145\/1882291.1882301"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: On interference abstractions. In: POPL (2011)","DOI":"10.1145\/1926385.1926433"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Torlak, E., Vaziri, M., Dolby, J.: MemSAT: Checking axiomatic specifications of memory models. In: PLDI (2010)","DOI":"10.1145\/1806596.1806635"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"G. Winskel","year":"1987","unstructured":"Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0255, pp. 325\u2013392. Springer, Heidelberg (1987)"}],"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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:43:06Z","timestamp":1557931386000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}