{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:12Z","timestamp":1775873532260,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221095","type":"print"},{"value":"9783642221101","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_28","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"356-371","source":"Crossref","is-referenced-by-count":26,"title":["Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Alastair","family":"Donaldson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Kaiser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Alglave, J.: A Shared Memory Poetics. PhD thesis, Universit\u00e9 Paris 7 and INRIA (2010), http:\/\/moscova.inria.fr\/~alglave\/these"},{"key":"28_CR2","volume-title":"Optimizing Compilers for Modern Architectures","author":"R. Allen","year":"2002","unstructured":"Allen, R., Kennedy, K.: Optimizing Compilers for Modern Architectures. Morgan Kaufmann, San Francisco (2002)"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-540-24730-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 388\u2013403. Springer, Heidelberg (2004)"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (PLDI), pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Principles of Programming Languages (POPL), pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Context-aware counter abstraction. In: Formal Methods in System Design (FMSD), vol.\u00a036(3), pp. 223\u2013245 (2010)","DOI":"10.1007\/s10703-010-0096-7"},{"key":"28_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. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 334\u2013349. Springer, Heidelberg (2006)"},{"key":"28_CR8","unstructured":"Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: a software model checking approach. In: Formal Methods in Computer-Aided Design, FMCAD (2010)"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, JACM (2003)","DOI":"10.1145\/876638.876643"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. In: Formal Methods in System Design (FMSD), pp. 105\u2013127 (2004)","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs (extended technical report). In: CoRR, pp. 1102\u20132330 (2011)","DOI":"10.1007\/978-3-642-22110-1_28"},{"key":"28_CR12","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":"28_CR13","first-page":"331","volume-title":"POPL","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL, pp. 331\u2013344. ACM Press, New York (2011)"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R.: Race checking by context inference. In: Programming Language Design and Implementation (PLDI), pp. 1\u201313 (2004)","DOI":"10.1145\/996841.996844"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T. Henzinger","year":"2003","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"key":"28_CR16","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1109\/12.947002","volume":"50","author":"J. Lee","year":"2001","unstructured":"Lee, J., Padua, D.: Hiding relaxed memory consistency with a compiler. IEEE Transactions on Computers\u00a050, 824\u2013833 (2001)","journal-title":"IEEE Transactions on Computers"},{"key":"28_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Boston (1993)"},{"issue":"1","key":"28_CR18","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"J. Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey, J., Scott, M.: Algorithms for scalable synchronization on shared-memory multiprocessors. Transactions on Computer Systems (TOCS)\u00a09(1), 21\u201365 (1991)","journal-title":"Transactions on Computer Systems (TOCS)"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Morris, J.: A general axiom of assignment. In: Theoretical Foundations of Programming Methodology. Lecture Notes of an International Summer School, pp. 25\u201334. D. Reidel Publishing Company (1982)","DOI":"10.1007\/978-94-009-7893-5_3"},{"key":"28_CR20","volume-title":"Java Concurrency in Practice","author":"T. Peierls","year":"2005","unstructured":"Peierls, T., Goetz, B., Bloch, J., Bowbeer, J., Lea, D., Holmes, D.: Java Concurrency in Practice. Addison-Wesley Professional, Reading (2005)"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Rugina, R., Rinard, M.C.: Pointer analysis for multithreaded programs. In: PLDI, pp. 77\u201390 (1999)","DOI":"10.1145\/301618.301645"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/978-3-642-16901-4_35","volume-title":"Formal Methods and Software Engineering","author":"N. Timm","year":"2010","unstructured":"Timm, N., Wehrheim, H.: On symmetries and spotlights \u2013 verifying parameterised systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 534\u2013548. Springer, Heidelberg (2010)"}],"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-22110-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T13:41:14Z","timestamp":1560346874000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}