{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:26Z","timestamp":1775873666732,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540770497","type":"print"},{"value":"9783540770503","type":"electronic"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-77050-3_4","type":"book-chapter","created":{"date-parts":[[2007,11,26]],"date-time":"2007-11-26T03:39:22Z","timestamp":1196048362000},"page":"23-51","source":"Crossref","is-referenced-by-count":17,"title":["Program Analysis Using Weighted Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Reps","sequence":"first","affiliation":[]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[]},{"given":"Nick","family":"Kidd","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G.: WYSINWYX: What You See Is Not What You eXecute. PhD thesis, Comp. Sci. Dept. Univ. of Wisconsin, Madison, WI, August 2007, Tech. Rep. 1603","DOI":"10.1007\/978-3-540-69149-5_22"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Comp. Construct., pp. 5\u201323 (2004)","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.-H., Teitelbaum, T.: Model checking x86 executables with CodeSurfer\/x86 and WPDS++. In: Computer Aided Verif. (2005)","DOI":"10.1007\/11513988_17"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN Model Checking and Software Verification. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A path-sensitive interprocedural dataflow engine. In: Prog. Analysis for Softw. Tools and Eng., 97\u2013103 (June 2001)","DOI":"10.1145\/379605.379690"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","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, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Princ. of Prog. Lang., pp. 62\u201373 (2003)","DOI":"10.1145\/640128.604137"},{"issue":"6","key":"4_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp.\u00a0C-35(6), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Comp."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"B\u00fcchi, J.R.: Finite Automata, their Algebras and Grammars. In: Siefkes, D. (ed.), Springer, Heidelberg (1988)","DOI":"10.1007\/978-1-4613-8853-1"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"CONCUR \u201992","author":"O. Burkart","year":"1992","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 123\u2013137. Springer, Heidelberg (1992)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Int. Conf. on Softw. Eng. (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. Tools and Algs. for the Construct. and Anal. of Syst. (2006)","DOI":"10.1007\/11691372_22"},{"key":"4_CR13","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: Princ. of Prog. Lang., pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"4_CR14","first-page":"237","volume-title":"Formal Descriptions of Programming Concepts","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E.J. (ed.) Formal Descriptions of Programming Concepts, IFIP WG 2.2, St. Andrews, Canada, August 1977, pp. 237\u2013277. North-Holland, Amsterdam (1978)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Princ. of Prog. Lang., pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Princ. of Prog. Lang., pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","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, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Elec. Notes in Theor. Comp. Sci. 9 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"4_CR19","unstructured":"Gopan, D.: Numeric program analysis techniques with applications to array analysis and library summarization. PhD thesis, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI, August 2007. Tech. Rep. 1602"},{"key":"4_CR20","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":"4_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Necula, G.C.: Precise interprocedural analysis using random interpretation. In: Princ. of Prog. Lang. (2005)","DOI":"10.1145\/1040305.1040332"},{"issue":"3","key":"4_CR22","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":"4_CR23","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationship among variables of a program. Acta Inf.\u00a06, 133\u2013151 (1976)","journal-title":"Acta Inf."},{"key":"4_CR24","unstructured":"Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: AC++ library for weighted pushdown systems (2004), http:\/\/www.cs.wisc.edu\/wpis\/wpds++\/"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Princ. of Prog. Lang., pp. 194\u2013206 (1973)","DOI":"10.1145\/512927.512945"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Comp. Construct., pp. 125\u2013140 (1992)","DOI":"10.1007\/3-540-55984-1_13"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Kodumal, J., Aiken, A.: Banshee: A scalable constraint-based analysis toolkit. In: Static Analysis Symp. (2005)","DOI":"10.1007\/11547662_16"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Lal, A., Lim, J., Polishchuk, M., Liblit, B.: Path optimization in programs and its application to debugging. In: European Symp. on Programming (2006)","DOI":"10.1007\/11693024_17"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Lal, A., Reps, T.: Improving pushdown system model checking. In: Computer Aided Verif. (2006)","DOI":"10.1007\/11817963_32"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Computer Aided Verif. (2005)","DOI":"10.1007\/11513988_44"},{"key":"4_CR31","unstructured":"Lal, A.,Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. Tech. Rep. TR-1598, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI (July 2007)"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Landi, W., Ryder, B.G.: Pointer induced aliasing: A problem classification. In: Princ. of Prog. Lang., January 1991, pp. 93\u2013103 (1991)","DOI":"10.1145\/99583.99599"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Martin, F.: PAG \u2013 An efficient program analyzer generator. Softw. Tools for Tech. Transfer (1998)","DOI":"10.1007\/s100090050017"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Princ. of Prog. Lang. (2004)","DOI":"10.1145\/964001.964029"},{"key":"4_CR35","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":"4_CR36","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Prog. Lang. Design and Impl. (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"4_CR37","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":"4_CR38","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Tools and Algs. for the Construct. and Anal. of Syst. (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: Keep it simple and sequential. In: Prog. Lang. Design and Impl. (2004)","DOI":"10.1145\/996841.996845"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Princ. of Prog. Lang., pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"4_CR41","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"},{"issue":"1\u20132","key":"4_CR42","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T. Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. of Comp. Prog.\u00a058(1\u20132), 206\u2013263 (2005)","journal-title":"Sci. of Comp. Prog."},{"key":"4_CR43","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":"4_CR44","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany (July 2002)"},{"key":"4_CR45","unstructured":"Schwoon, S.: WPDS: A library for weighted pushdown systems (2003), http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/wpds\/"},{"key":"4_CR46","unstructured":"Schwoon, S., Jha, S., Reps, T., Stubblebine, S.: On generalized authorization problems. In: Comp. Sec. Found. Workshop (2003)"},{"key":"4_CR47","first-page":"189","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: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, (ch. 7), pp. 189\u2013234. Prentice-Hall, Englewood Cliffs, NJ (1981)"},{"key":"4_CR48","doi-asserted-by":"crossref","unstructured":"Whaley, J., Avots, D., Carbin, M., Lam, M.S.: Using Datalog with Binary Decision Diagrams for program analysis. In: Asian Symp. on Prog. Lang. and Systems (2005)","DOI":"10.1007\/11575467_8"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77050-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T18:48:29Z","timestamp":1684090109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77050-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540770497","9783540770503"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77050-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007]]}}}