{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:11:41Z","timestamp":1774987901806,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662445839","type":"print"},{"value":"9783662445846","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44584-6_11","type":"book-chapter","created":{"date-parts":[[2014,8,23]],"date-time":"2014-08-23T01:21:03Z","timestamp":1408756863000},"page":"141-155","source":"Crossref","is-referenced-by-count":14,"title":["Lost in Abstraction: Monotonicity in Multi-threaded Programs"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Kaiser","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A.: Well (and better) quasi-ordered transition systems. B. Symb. Log. (2010)","DOI":"10.2178\/bsl\/1294171129"},{"key":"11_CR2","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems of infinite-state systems. In: LICS (1996)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Monotonic abstraction in parameterized verification. ENTCS (2008)","DOI":"10.1016\/j.entcs.2008.12.027"},{"key":"11_CR4","volume-title":"Concurrent programming: principles and practice","author":"G.R. Andrews","year":"1991","unstructured":"Andrews, G.R.: Concurrent programming: principles and practice. Benjamin-Cummings Publishing Co., Inc., Redwood City (1991)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-31980-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.D. Bingham","year":"2005","unstructured":"Bingham, J.D., Hu, A.J.: Empirically efficient verification for a class of infinite-state systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 77\u201392. Springer, Heidelberg (2005)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11691372_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chaki","year":"2006","unstructured":"Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 334\u2013349. Springer, Heidelberg (2006)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: TOPLAS (1994)","DOI":"10.1145\/186025.186051"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Verification of Boolean programs with unbounded thread creation. Theoretical Comput. Sci. (2007)","DOI":"10.1109\/FMCAD.2006.24"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: Counterexample-guided abstraction refinement for symmetric concurrent programs. In: FMSD (2012)","DOI":"10.1007\/s10703-012-0155-3"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-12002-2_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Dr\u00e4ger","year":"2010","unstructured":"Dr\u00e4ger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: A certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 271\u2013274. Springer, Heidelberg (2010)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. In: POPL (2012)","DOI":"10.1145\/2103656.2103693"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-39799-8_12","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2013","unstructured":"Farzan, A., Kincaid, Z.: duet: Static analysis for unbounded parallelism. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 191\u2013196. Springer, Heidelberg (2013)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: POPL (2013)","DOI":"10.1145\/2429069.2429086"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Comput. Sci. (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191\u2013202. ACM (2002)","DOI":"10.1145\/565816.503291"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"German, S., Sistla, P.: Reasoning about systems with many processes. JACM (1992)","DOI":"10.1145\/146637.146681"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL (2011)","DOI":"10.1145\/1926385.1926424"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI (2004)","DOI":"10.1145\/996841.996844"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Lost in abstraction: Monotonicity in multi-threaded programs (extended technical report). CoRR (2014)","DOI":"10.1007\/978-3-662-44584-6_11"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-540-24622-0_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 267\u2013281. Springer, Heidelberg (2004)"},{"key":"11_CR23","unstructured":"Malkis, A.: Cartesian Abstraction and Verification of Multithreaded Programs. PhD thesis, Albert-Ludwigs-Universit\u00e4t Freiburg (2010)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-33125-1_12","volume-title":"Static Analysis","author":"A. Sanchez","year":"2012","unstructured":"Sanchez, A., Sankaranarayanan, S., S\u00e1nchez, C., Chang, B.-Y.E.: Invariant generation for parametrized systems using self-reflection. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 146\u2013163. Springer, Heidelberg (2012)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/978-3-642-14295-6_54","volume-title":"Computer Aided Verification","author":"S. La Torre","year":"2010","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 629\u2013644. Springer, Heidelberg (2010)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: ASE (2007)","DOI":"10.1145\/1321631.1321719"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2014 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44584-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T17:10:29Z","timestamp":1558977029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44584-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662445839","9783662445846"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44584-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}