{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T09:31:44Z","timestamp":1791192704863,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642388552","type":"print"},{"value":"9783642388569","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_20","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T00:05:28Z","timestamp":1371254728000},"page":"366-387","source":"Crossref","is-referenced-by-count":6,"title":["Static Provenance Verification for Message Passing Programs"],"prefix":"10.1007","author":[{"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zilong","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313\u2013321. IEEE (1996)"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Barth, A., Mitchell, J., Datta, A., Sundaram, S.: Privacy and utility in business processes. In: CSF, pp. 279\u2013294. IEEE (2007)","DOI":"10.1109\/CSF.2007.26"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/3-540-44503-X_20","volume-title":"Database Theory - ICDT 2001","author":"P. Buneman","year":"2000","unstructured":"Buneman, P., Khanna, S., Tan, W.-C.: Why and where: A characterization of data provenance. In: Van den Bussche, J., Vianu, V. (eds.) ICDT 2001. LNCS, vol.\u00a01973, pp. 316\u2013330. Springer, Heidelberg (2000)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Chaki, S., Rajamani, S., Rehof, J.: Types as models: model checking message-passing programs. In: POPL, pp. 45\u201357. ACM (2002)","DOI":"10.1145\/565816.503278"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"1301","DOI":"10.1017\/S0960129511000211","volume":"21","author":"J. Cheney","year":"2011","unstructured":"Cheney, J., Ahmed, A., Acar, U.: Provenance as dependency analysis. Math. Struct. in Computer Science\u00a021, 1301\u20131337 (2011)","journal-title":"Math. Struct. in Computer Science"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/357775.357777","volume":"25","author":"Y. Cui","year":"2000","unstructured":"Cui, Y., Widom, J., Wiener, J.: Tracing the lineage of view data in a warehousing environment. ACM TODS\u00a025, 179\u2013227 (2000)","journal-title":"ACM TODS"},{"key":"20_CR7","unstructured":"Durak, B.: JSure, \n                  \n                    https:\/\/github.com\/berke\/jsure"},{"issue":"1-2","key":"20_CR8","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"20_CR9","first-page":"275","volume":"88","author":"P. Ganty","year":"2008","unstructured":"Ganty, P., Raskin, J.-F., Begin, L.V.: From many places to few: Automatic abstraction refinement for Petri nets. Fund. Informaticae\u00a088(3), 275\u2013305 (2008)","journal-title":"Fund. Informaticae"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-30538-5_24","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"G. Geeraerts","year":"2004","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 287\u2013298. Springer, Heidelberg (2004)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Green, T., Karvounarakis, G., Tannen, V.: Provenance semirings. In: PODS, pp. 31\u201340. ACM (2007)","DOI":"10.1145\/1265530.1265535"},{"key":"20_CR13","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc (3) 2, 326\u2013336 (1952)","journal-title":"Proc. London Math. Soc (3)"},{"issue":"5","key":"20_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The Spin model checker. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Huang, Y.-W., Yu, F., Hang, C., Tsai, C.-H., Lee, D.-T., Kuo, S.-Y.: Securing web application code by static analysis and runtime protection. In: WWW, pp. 40\u201352 (2004)","DOI":"10.1145\/988672.988679"},{"key":"20_CR16","unstructured":"Jan\u00e1k, J.: Issue tracking systems. Diplomov\u00e1 pr\u00e1ce, Masarykova univerzita, Fakulta informatiky (2009)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL 2007, pp. 339\u2013350. ACM (2007)","DOI":"10.1145\/1190215.1190266"},{"key":"20_CR18","unstructured":"Lipton, R.: The reachability problem is exponential-space hard. Technical Report\u00a062, Department of Computer Science, Yale University (1976)"},{"key":"20_CR19","unstructured":"Livshits, B., Lam, M.: Finding security errors in Java programs with static analysis. In: Usenix Security Symposium, pp. 271\u2013286 (2005)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-46562-6_18","volume-title":"Perspectives of System Informatics","author":"I.A. Lomazova","year":"2000","unstructured":"Lomazova, I.A., Schnoebelen, P.: Some decidability results for nested Petri nets. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol.\u00a01755, pp. 208\u2013220. Springer, Heidelberg (2000)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-642-14295-6_19","volume-title":"Computer Aided Verification","author":"R. Meyer","year":"2010","unstructured":"Meyer, R., Strazny, T.: Petruchio: From dynamic networks to nets. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 175\u2013179. Springer, Heidelberg (2010)"},{"key":"20_CR22","unstructured":"Minsky, M.: Finite and Infinite Machines. Prentice-Hall (1967)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1,\u2009\u221e\u2009)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"issue":"2","key":"20_CR24","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science\u00a06(2), 223\u2013231 (1978)","journal-title":"Theoretical Computer Science"},{"key":"20_CR25","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE J. Selected Areas in Communications\u00a021, 5\u201319 (2003)","journal-title":"IEEE J. Selected Areas in Communications"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-642-15155-2_54","volume-title":"Mathematical Foundations of Computer Science 2010","author":"P. Schnoebelen","year":"2010","unstructured":"Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol.\u00a06281, pp. 616\u2013628. Springer, Heidelberg (2010)"},{"key":"20_CR27","unstructured":"Souilah, I., Francalanza, A., Sassone, V.: A formal model of provenance in distributed systems. In: Workshop on the Theory and Practice of Provenance (2009)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T00:54:35Z","timestamp":1557795275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}