{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:10:36Z","timestamp":1763467836211},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787990"},{"type":"electronic","value":"9783540788003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78800-3_20","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T04:26:19Z","timestamp":1207110379000},"page":"282-298","source":"Crossref","is-referenced-by-count":37,"title":["Interprocedural Analysis of Concurrent Programs Under a Context Bound"],"prefix":"10.1007","author":[{"given":"Akash","family":"Lal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicholas","family":"Kidd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, Springer, Heidelberg (1997)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11590156_28","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Esparza, J., Schwoon, S., Strejcek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 348\u2013359. Springer, Heidelberg (2005)"},{"key":"20_CR4","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":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-73368-3_24","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 207\u2013220. Springer, Heidelberg (2007)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 473\u2013487. Springer, Heidelberg (2005)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"B\u00fcchi, J.R.: Finite Automata, their Algebras and Grammars. Springer, New York(1988)","DOI":"10.1007\/978-1-4613-8853-1"},{"issue":"1","key":"20_CR8","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"Caucal, D.: On the regular structure of prefix rewriting. TCS\u00a0106(1), 61\u201386 (1992)","journal-title":"TCS"},{"key":"20_CR9","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":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electronic Notes in Theoretical Comp. Sci.\u00a09 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"20_CR13","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: POPL (2007)","DOI":"10.1145\/1190216.1190262"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-74061-2_13","volume-title":"Static Analysis","author":"A. Lal","year":"2007","unstructured":"Lal, A., Kidd, N., Reps, T., Touili, T.: Abstract error projection. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 200\u2013217. Springer, Heidelberg (2007)"},{"key":"20_CR16","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. TR-1598, University of Wisconsin (July 2007)"},{"key":"20_CR17","unstructured":"Mohri, M., Pereira, F., Riley, M.: Weighted automata in text and speech processing. In: ECAI (1996)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"M. Mohri","year":"2000","unstructured":"Mohri, M., Pereira, F., Riley, M.: The design principles of a weighted finite-state transducer library. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, Springer, Heidelberg (2000)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)","DOI":"10.1145\/964001.964029"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"20_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_28","volume-title":"Computer Aided Verification","author":"G. Patin","year":"2007","unstructured":"Patin, G., Sighireanu, M., Touili, T.: Spade: Verification of multithreaded dynamic and recursive programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, Springer, Heidelberg (2007)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"20_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":"20_CR25","doi-asserted-by":"crossref","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. In: TOPLAS (2000)","DOI":"10.1145\/349214.349241"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL (1995)","DOI":"10.1145\/199448.199462"},{"key":"20_CR27","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.21236\/ADA449102"},{"key":"20_CR28","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany (July 2002)"},{"key":"20_CR29","unstructured":"Wikipedia. Kronecker product, http:\/\/en.wikipedia.org\/wiki\/Kronecker_product"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78800-3_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:22:46Z","timestamp":1619508166000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78800-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787990","9783540788003"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3_20","relation":{},"subject":[]}}