{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:45:01Z","timestamp":1725565501108},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642157684"},{"type":"electronic","value":"9783642157691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_22","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T02:09:40Z","timestamp":1284343780000},"page":"356-372","source":"Crossref","is-referenced-by-count":6,"title":["Thread-Modular Counterexample-Guided Abstraction Refinement"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Malkis","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"22_CR1","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1142\/S0129054103001893","volume":"14","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. Int. J. Found. Comput. Sci.\u00a014(4), 551 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"22_CR2","volume-title":"Pthreads programming","author":"J.P.F. Bradford Nichols","year":"1996","unstructured":"Bradford Nichols, J.P.F., Buttlar, D.: Pthreads programming. O\u2019Reilly & Associates, Inc, Sebastopol (1996)"},{"key":"22_CR3","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.M., Kidd, N., Reps, T.W., 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":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 126\u2013141. Springer, Heidelberg (2005)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-73368-3_9","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2007","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 55\u201367. Springer, Heidelberg (2007)"},{"key":"22_CR6","first-page":"243","volume-title":"Automatic Program Construction Techniques","author":"P. Cousot","year":"1984","unstructured":"Cousot, P., Cousot, R.: Invariance proof methods andanalysis techniques for parallel programs. In: Automatic Program Construction Techniques, pp. 243\u2013271. Macmillan, Basingstoke (1984)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Ganty, P., Raskin, J.-F.: Fixpoint-guided abstraction refinements. In: Nielson and Fil\u00e9 [26], pp. 333\u2013348","DOI":"10.1007\/978-3-540-74061-2_21"},{"key":"22_CR8","unstructured":"de Roever, W.-P.: A compositional approach to concurrency and its applications. Manuscript (2003)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/11547662_10","volume-title":"Static Analysis","author":"J. Esparza","year":"2005","unstructured":"Esparza, J., Ganty, P., Schwoon, S.: Locality-based abstractions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 118\u2013134. Springer, Heidelberg (2005)"},{"issue":"1-3","key":"22_CR10","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci.\u00a0338(1-3), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"22_CR12","unstructured":"Ganty, P.: The Fixpoint Checking Problem: An Abstraction Renement Perspective. PhD thesis, Universit\u00e9 Libre de Bruxelles (2007)"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/996841.996844","volume-title":"PLDI","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Pugh, W., Chambers, C. (eds.) PLDI, pp. 1\u201313. ACM, New York (2004)"},{"key":"22_CR14","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.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., 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":"22_CR15","unstructured":"Holzmann, G.: The Spin model checker: Primer and reference manual. Addison-Wesley, Reading ISBN 0-321-22862-6, http:\/\/www.spinroot.com"},{"issue":"4","key":"22_CR16","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-642-00768-2_12","volume-title":"TACAS","author":"V. Kahlon","year":"2009","unstructured":"Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS. LNCS, vol.\u00a05505, pp. 124\u2013138. Springer, Heidelberg (2009)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-70545-1_7","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2008","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"22_CR19","unstructured":"Leroy, X.: Pthreads linux manual pages, http:\/\/www.digipedia.pl\/man\/pthread_mutex_init.3thr.html"},{"key":"22_CR20","unstructured":"Malkis, A.: Cartesian Abstraction and Verification of Multithreaded Programs. PhD thesis, Albert-Ludwigs-Universit\u00e4t Freiburg (2010)"},{"key":"22_CR21","unstructured":"Malkis, A., Podelski, A.: Refinement with exceptions. Technical report (2008), http:\/\/www.informatik.uni-freiburg.de\/~alexmalk\/refinementWithExceptions_techrep.pdf"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification and Cartesian abstraction. In: Presentation at TV 2006 (2006)","DOI":"10.1007\/11921240_13"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/11921240_13","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"A. Malkis","year":"2006","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is Cartesian abstract interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 183\u2013197. Springer, Heidelberg (2006)"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Precise thread-modular verification. In: Nielson and Fil\u00e9 [26], pp. 218\u2013232","DOI":"10.1007\/978-3-540-74061-2_14"},{"key":"22_CR25","unstructured":"Mueller, F.: Implementing POSIX threads under UNIX: Description of work in progress. In: Proceedings of the 2nd Software Engineering Research Forum, Melbourne, Florida (November 1992)"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","year":"2007","unstructured":"Nielson, H.R., Fil\u00e9, G. (eds.): SAS 2007. LNCS, vol.\u00a04634. Springer, Heidelberg (2007)"},{"key":"22_CR27","unstructured":"Owicki, S.S.: Axiomatic Proof Techniques For Parallel Programs. PhD thesis, Cornell University, Department of Computer Science, TR 75-251 (July 1975)"},{"key":"22_CR28","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf.\u00a06, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"key":"22_CR29","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":"22_CR30","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/996841.996845","volume-title":"PLDI 2004","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: PLDI 2004, pp. 14\u201324. ACM, New York (2004)"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Giacobazzi, F.S.R., Ranzato, F.: Making abstract interpretations complete. JACM (2000)","DOI":"10.1145\/333979.333989"},{"key":"22_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-540-78163-9_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Ranzato","year":"2008","unstructured":"Ranzato, F., Rossi-Doria, O., Tapparo, F.: A forward-backward abstraction refinement algorithm. In: Logozzo, F., Peled, D., Zuck, L. D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 248\u2013262. Springer, Heidelberg (2008)"},{"issue":"1","key":"22_CR33","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1093\/logcom\/exl035","volume":"17","author":"F. Ranzato","year":"2007","unstructured":"Ranzato, F., Tapparo, F.: Generalized strong preservation by abstract interpretation. J. Log. Comput.\u00a017(1), 157\u2013197 (2007)","journal-title":"J. Log. Comput."},{"key":"22_CR34","unstructured":"Shankar, A.U.: Peterson\u2019s mutual exclusion algorithm (2003), http:\/\/www.cs.umd.edu\/~shankar\/712-S03\/mutex-peterson.ps"},{"key":"22_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"F.I. Vineet Kahlon","year":"2005","unstructured":"Vineet Kahlon, F.I., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 505\u2013518. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:40:19Z","timestamp":1606167619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}