{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:14:31Z","timestamp":1748751271461,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319287652"},{"type":"electronic","value":"9783319287669"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-28766-9_3","type":"book-chapter","created":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T12:09:44Z","timestamp":1451909384000},"page":"32-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Data Tracking in Parameterized Systems"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,5]]},"reference":[{"issue":"3","key":"3_CR1","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1016\/j.ic.2010.11.003","volume":"209","author":"PA Abdulla","year":"2011","unstructured":"Abdulla, P.A., Delzanno, G., Van Begin, L.: A classification of the expressive power of well-structured transition systems. Inf. Comput. 209(3), 248\u2013279 (2011)","journal-title":"Inf. Comput."},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-41157-1_5","volume-title":"Trustworthy Global Computing","author":"A Armando","year":"2013","unstructured":"Armando, A., Costa, G., Merlo, A.: Formal modeling and reasoning about the android security framework. In: Palamidessi, C., Ryan, M.D. (eds.) TGC 2012. LNCS, vol. 8191, pp. 64\u201381. Springer, Heidelberg (2013)"},{"issue":"4","key":"3_CR3","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/JCS-2012-0461","volume":"20","author":"A Armando","year":"2012","unstructured":"Armando, A., Ranise, S.: Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving. J. Comput. Secur. 20(4), 309\u2013352 (2012)","journal-title":"J. Comput. Secur."},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-71389-0_4","volume-title":"Foundations of Software Science and Computational Structures","author":"M Bartoletti","year":"2007","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.-L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 32\u201347. Springer, Heidelberg (2007)"},{"issue":"6","key":"3_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1552309.1552313","volume":"31","author":"Massimo Bartoletti","year":"2009","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Local policies for resource usage analysis. ACM TOPLAS, vol. 31(6) (2009)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"3_CR7","first-page":"710","volume":"25","author":"M Bartoletti","year":"2015","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. MSCS 25(3), 710\u2013763 (2015)","journal-title":"MSCS"},{"key":"3_CR8","unstructured":"Bozzano, M.: A Logic-Based Approach to Model Checking of Parameterized and Infinite-State Systems, Ph.D. thesis, DISI, University of Genova, June 2002"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-38592-6_20","volume-title":"Formal Techniques for Distributed Systems","author":"M Bugliesi","year":"2013","unstructured":"Bugliesi, M., Calzavara, S., Span\u00f2, A.: Lintent: towards security type-checking of android applications. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 289\u2013304. Springer, Heidelberg (2013)"},{"key":"3_CR10","first-page":"65","volume":"76","author":"G Delzanno","year":"2002","unstructured":"Delzanno, G.: An overview of MSR(C): A CLP-based framework for the symbolic verification of parameterized concurrent systems. ENTCS 76, 65\u201382 (2002)","journal-title":"ENTCS"},{"issue":"1\u20132","key":"3_CR11","first-page":"67","volume":"7","author":"G Delzanno","year":"2007","unstructured":"Delzanno, G.: Constraint-based automatic verification of abstract models of multithreaded programs. TPLP 7(1\u20132), 67\u201391 (2007)","journal-title":"TPLP"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/j.tcs.2012.09.021","volume":"467","author":"G Delzanno","year":"2013","unstructured":"Delzanno, G., Rosa-Velardo, F.: On the coverability and reachability languages of monotonic extensions of petri nets. Theor. Comput. Sci. 467, 12\u201329 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR13","unstructured":"Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS 2012, pp. 289\u2013300 (2012)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-15375-4_22","volume-title":"CONCUR 2010 - Concurrency Theory","author":"G Delzanno","year":"2010","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313\u2013327. Springer, Heidelberg (2010)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-19805-2_30","volume-title":"Foundations of Software Science and Computational Structures","author":"G Delzanno","year":"2011","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 441\u2013455. Springer, Heidelberg (2011)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS, pp. 70\u201380 (1998)","DOI":"10.1109\/LICS.1998.705644"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352\u2013359 (1999)","DOI":"10.1109\/LICS.1999.782630"},{"issue":"3","key":"3_CR18","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"issue":"3","key":"3_CR19","first-page":"251","volume":"88","author":"R Lazic","year":"2008","unstructured":"Lazic, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Inform. 88(3), 251\u2013274 (2008)","journal-title":"Fundam. Inform."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Meyer, R., Wang, Z.: Provenance verification. In: RP, pp. 21\u201322 (2013)","DOI":"10.1007\/978-3-642-41036-9_3"},{"issue":"1","key":"3_CR21","first-page":"24","volume":"42","author":"S Ranise","year":"2013","unstructured":"Ranise, S.: Symbolic backward reachability with effectively propositional logic - applications to security policy analysis. FMSD 42(1), 24\u201345 (2013)","journal-title":"FMSD"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-319-11851-2_10","volume-title":"Security and Trust Management","author":"S Ranise","year":"2014","unstructured":"Ranise, S., Traverso, R.: ALPS: an action language for policy specification and automated safety analysis. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 146\u2013161. Springer, Heidelberg (2014)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-02424-5_6","volume-title":"Applications and Theory of Petri Nets","author":"F Rosa-Velardo","year":"2009","unstructured":"Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability results for restricted models of petri nets with name creation and replication. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 63\u201382. Springer, Heidelberg (2009)"},{"key":"3_CR24","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. 6281, pp. 616\u2013628. Springer, Heidelberg (2010)"},{"issue":"2\u20133","key":"3_CR25","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/j.cose.2010.08.002","volume":"30","author":"SD Stoller","year":"2011","unstructured":"Stoller, S.D., Yang, P., Gofman, M.I., Ramakrishnan, C.R.: Symbolic reachability analysis for parameterized administrative role-based access control. Comput. Secur. 30(2\u20133), 148\u2013164 (2011)","journal-title":"Comput. Secur."},{"issue":"1","key":"3_CR26","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1145\/1925844.1926420","volume":"46","author":"Nikos Tzevelekos","year":"2011","unstructured":"Tzevelekos, N.: Fresh-register automata. In: POPL 2011, pp. 295\u2013306 (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-37075-5_2","volume-title":"Foundations of Software Science and Computation Structures","author":"N Tzevelekos","year":"2013","unstructured":"Tzevelekos, N., Grigore, R.: History-register automata. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 17\u201333. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-28766-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:57:02Z","timestamp":1748739422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-28766-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319287652","9783319287669"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-28766-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"5 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}