{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T14:15:11Z","timestamp":1791296111930,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540330561","type":"print"},{"value":"9783540330578","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11691372_22","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T09:22:26Z","timestamp":1143537746000},"page":"334-349","source":"Crossref","is-referenced-by-count":49,"title":["Verifying Concurrent Message-Passing C Programs with Recursive Calls"],"prefix":"10.1007","author":[{"given":"S.","family":"Chaki","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"E.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"N.","family":"Kidd","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T.","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T.","family":"Touili","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. TOPLAS\u00a022, 416\u2013430 (2000)","journal-title":"TOPLAS"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 14\u201330. Springer, Heidelberg (1999)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 324. Springer, Heidelberg (2001)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: CONCUR (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: Infinity (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL (2003)","DOI":"10.1145\/604131.604137"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. Int. J. Found. of Comp. Sci (2003)","DOI":"10.1145\/604131.604137"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, p. 486. Springer, Heidelberg (1997)"},{"key":"22_CR10","volume-title":"Computer-aided verification of coordinating processes: The automatatheoretic approach.","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-aided verification of coordinating processes: The automatatheoretic approach. Princeton University Press, Princeton (1994)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"582","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, p. 582. Springer, Heidelberg (2000)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, p. 103. Springer, Heidelberg (2001)"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"22_CR15","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TUM (2002)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. Tech. Rep. 1532, Univ. of Wisconsin (2005)","DOI":"10.1007\/11691372_22"},{"key":"22_CR17","unstructured":"Necula, G., McPeak, S., Weimer, W., Liblit, B., To, R., Bhargava, A.: C intermediate lang (2001), http:\/\/manju.cs.berkeley.edu\/cil"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Morris, J.: Assignment and linked data structures. In: Theoretical Foundations of Programming Methodology, D. Reidel Publishing Co (1982)","DOI":"10.1007\/978-94-009-7893-5_4"},{"key":"22_CR19","unstructured":"Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University (1980)"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_11","volume-title":"Static Analysis","author":"T. Reps","year":"2003","unstructured":"Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: SCP, vol.\u00a058 (2005)","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"22_CR22","unstructured":"Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ library for weighted pushdown systems (2004), http:\/\/www.cs.wisc.edu\/wpis\/wpds++\/"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/11513988_18","volume-title":"Computer Aided Verification","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Ivers, J., Sharygina, N., Wallnau, K.: The ComFoRT reasoning framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 164\u2013169. Springer, Heidelberg (2005)"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: Keep it simple and sequential. In: PLDI (2004)","DOI":"10.1145\/996841.996845"},{"key":"22_CR25","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_CR26","doi-asserted-by":"crossref","unstructured":"Kung, H., Lehman, P.: Concurrent manipulation of binary search trees. TODS\u00a05 (1980)","DOI":"10.1145\/320613.320619"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rajamani, S., Rehof, J.: Summarizing procedures in concurrent programs. In: POPL (2004)","DOI":"10.1145\/964001.964022"},{"key":"22_CR28","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":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivancic, F., 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","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691372_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T13:19:25Z","timestamp":1555507165000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691372_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330561","9783540330578"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/11691372_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}