{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:13:51Z","timestamp":1774988031295,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540272311","type":"print"},{"value":"9783540316862","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_44","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:33:28Z","timestamp":1268400808000},"page":"434-448","source":"Crossref","is-referenced-by-count":43,"title":["Extended Weighted Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Akash","family":"Lal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gogul","family":"Balakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"44_CR1","volume-title":"Compilers: Principles, Techniques and Tools","author":"A.V. Aho","year":"1985","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1985)"},{"key":"44_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Int. Conf. on Comp. Construct. (2004)","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"44_CR3","first-page":"135","volume-title":"CONCUR","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: CONCUR, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"44_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: Symp. on Princ. of Prog. Lang., pp. 62\u201373 (2003)","DOI":"10.1145\/604131.604137"},{"key":"44_CR5","doi-asserted-by":"crossref","unstructured":"Chen, H., Wagner, D.: MOPS: An infrastructure for examining security properties of software. In: Conf. on Comp. and Commun. Sec. (November 2002)","DOI":"10.1145\/586110.586142"},{"key":"44_CR6","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku\u010dera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. In: TACAS, pp. 306\u2013339 (2001)","DOI":"10.1007\/3-540-45500-0_16"},{"key":"44_CR7","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, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"44_CR8","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems, 9th edn. Electronic Notes in Theoretical Computer Science, vol.\u00a09 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"44_CR9","doi-asserted-by":"crossref","unstructured":"Jensen, T., Le M\u00e9tayer, D., Thorn, T.: Verification of control flow based security properties. In: IEEE Symposium on Security and Privacy, pp. 89\u2013103 (1999)","DOI":"10.1109\/SECPRI.1999.766902"},{"issue":"3","key":"44_CR10","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BF00290339","volume":"7","author":"J.B. Kam","year":"1977","unstructured":"Kam, J.B., Ullman, J.D.: Monotone data flow analysis frameworks. Acta Inf.\u00a07(3), 305\u2013318 (1977)","journal-title":"Acta Inf."},{"key":"44_CR11","unstructured":"Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ library for weighted pushdown systems (2004)"},{"key":"44_CR12","doi-asserted-by":"crossref","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Int. Conf. on Comp. Construct., pp. 125\u2013140 (1992)","DOI":"10.1007\/3-540-55984-1_13"},{"key":"44_CR13","doi-asserted-by":"crossref","unstructured":"Landi, W., Ryder, B.: Pointer-induced aliasing: A problem classification. In: Symp. on Princ. of Prog. Lang., pp. 93\u2013103 (1991)","DOI":"10.1145\/99583.99599"},{"key":"44_CR14","doi-asserted-by":"crossref","unstructured":"Landi, W., Ryder, B.: A safe approximate algorithm for interprocedural pointer aliasing. In: Conf. on Prog. Lang. Design and Impl., pp. 235\u2013248 (1992)","DOI":"10.1145\/143103.143137"},{"key":"44_CR15","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Symp. on Princ. of Prog. Lang. (2004)","DOI":"10.1145\/964001.964029"},{"key":"44_CR16","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: European Symp. on Programming (2005)","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"44_CR17","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Symp. on Princ. of Prog. Lang., pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"44_CR18","doi-asserted-by":"crossref","unstructured":"Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Static Analysis Symp., pp. 189\u2013213 (2003)","DOI":"10.1007\/3-540-44898-5_11"},{"key":"44_CR19","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0304-3975(96)00072-2","volume":"167","author":"M. Sagiv","year":"1996","unstructured":"Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comp. Sci.\u00a0167, 131\u2013170 (1996)","journal-title":"Theor. Comp. Sci."},{"key":"44_CR20","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany (July 2002)"},{"key":"44_CR21","unstructured":"Schwoon, S.: Moped (2002), http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/"},{"key":"44_CR22","volume-title":"Comp. Sec. Found. Workshop","author":"S. Schwoon","year":"2003","unstructured":"Schwoon, S., Jha, S., Reps, T., Stubblebine, S.: On generalized authorization problems. In: Comp. Sec. Found. Workshop, Wash., DC, IEEE Comp. Soc., Los Alamitos (2003)"},{"key":"44_CR23","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"44_CR24","doi-asserted-by":"crossref","unstructured":"Whaley, J., Lam, M.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Conf. on Prog. Lang. Design and Impl., pp. 131\u2013144 (2004)","DOI":"10.1145\/996841.996859"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T12:06:51Z","timestamp":1739966811000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11513988_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}