{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:27:05Z","timestamp":1760056025999,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":103,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319568409"},{"type":"electronic","value":"9783319568416"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-56841-6_6","type":"book-chapter","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T13:00:33Z","timestamp":1491397233000},"page":"195-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Reasoning on Infinite Data Values: An Ongoing Quest"],"prefix":"10.1007","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,6]]},"reference":[{"key":"6_CR1","unstructured":"Alur, R., Cern\u00fd, P.: Expressiveness of streaming string transducers. In: Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics (LIPIcs), vol. 8, pp. 1\u201312 (2010)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Cerny, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 599\u2013610 (2011)","DOI":"10.1145\/1926385.1926454"},{"issue":"3","key":"6_CR3","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/2287718.2287727","volume":"13","author":"R Alur","year":"2012","unstructured":"Alur, R., Cern\u00fd, P., Weinstein, S.: Algorithmic analysis of array-accessing programs. ACM Trans. Comput. Log. 13(3), 27 (2012)","journal-title":"ACM Trans. Comput. Log."},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-31585-5_8","volume-title":"Automata, Languages, and Programming","author":"R Alur","year":"2012","unstructured":"Alur, R., D\u2019Antoni, L.: Streaming tree transducers. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012. LNCS, vol. 7392, pp. 42\u201353. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31585-5_8"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Durand-Gasselin, A., Trivedi, A.: From monadic second-order definable string transformations to transducers. In: Proceedings of the 28th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 458\u2013467 (2013)","DOI":"10.1109\/LICS.2013.52"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/978-3-642-54830-7_27","volume-title":"Foundations of Software Science and Computation Structures","author":"T Antonopoulos","year":"2014","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 411\u2013425. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54830-7_27"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Holik, L., Jonsson, B., Lengal, O., Trinh, C.Q., Vojnar, T.: Verification of heap manipulating programs with ordered data by extended forest automata. In: Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 224\u2013239 (2013)","DOI":"10.1007\/978-3-319-02444-8_17"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-00596-1_30","volume-title":"Foundations of Software Science and Computational Structures","author":"K Bansal","year":"2009","unstructured":"Bansal, K., Brochenin, R., Lozes, E.: Beyond shapes: lists with ordered data. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 425\u2013439. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00596-1_30"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). doi:10.1007\/11575467_5"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 178\u2013195. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-04081-8_13"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-33386-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u01cegoi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 167\u2013182. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33386-6_14"},{"issue":"4","key":"6_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/1970398.1970403","volume":"12","author":"M Bojanczyk","year":"2011","unstructured":"Bojanczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Logic 12(4), 27 (2011)","journal-title":"ACM Trans. Comput. Logic"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Fuhs, C., Gorogiannis, J.N., Perez, A.N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of the 29th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS) (2014)","DOI":"10.1145\/2603088.2603091"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., Klin, B., Lasota, S., Toru\u0144czyk, S.: Turing machines with atoms. In: Proceedings of the 28th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 183\u2013192 (2013)","DOI":"10.1109\/LICS.2013.24"},{"issue":"1","key":"6_CR15","first-page":"1","volume":"8","author":"M Bojanczyk","year":"2012","unstructured":"Bojanczyk, M., Lasota, S.: An extension of data automata that captures XPath. Log. Methods Comput. Sci. 8(1), 1\u201328 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS), pp. 7\u201316 (2006)","DOI":"10.1109\/LICS.2006.51"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-642-39992-3_3","volume-title":"Logic, Language, Information, and Computation","author":"M Boja\u0144czyk","year":"2013","unstructured":"Boja\u0144czyk, M.: Modelling infinite structures with atoms. In: Libkin, L., Kohlenbach, U., de Queiroz, R. (eds.) WoLLIC 2013. LNCS, vol. 8071, pp. 13\u201328. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39992-3_3"},{"issue":"4\u20135","key":"6_CR18","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1016\/j.tcs.2009.10.009","volume":"411","author":"H Bj\u00f6rklund","year":"2010","unstructured":"Bj\u00f6rklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4\u20135), 702\u2013715 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11786986_15","volume-title":"Automata, Languages and Programming","author":"M Boja\u0144czyk","year":"2006","unstructured":"Boja\u0144czyk, M., Samuelides, M., Schwentick, T., Segoufin, L.: Expressive power of pebble automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4051, pp. 157\u2013168. Springer, Heidelberg (2006). doi:10.1007\/11786986_15"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Log. Grundl. Math. 6, 66\u201392 (1960)","journal-title":"Z. Math. Log. Grundl. Math."},{"key":"6_CR21","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second-order arithmetic. In: Proceedings of the 1960 International Congress for Logic, Methodology and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)"},{"issue":"9","key":"6_CR22","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"6_CR23","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011)","journal-title":"J. ACM"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235\u2013249. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-23217-6_16"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-662-46681-0_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-F Chen","year":"2015","unstructured":"Chen, Y.-F., Hong, C.-D., Sinha, N., Wang, B.-Y.: Commutativity of reducers. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 131\u2013146. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_9"},{"issue":"2","key":"6_CR26","first-page":"1265","volume":"1","author":"R Chaiken","year":"2008","unstructured":"Chaiken, R., Jenkins, B., Larson, P.\u00c5., Ramsey, B., Shakib, D., Weaver, S., Zhou, J.: SCOPE: easy and efficient parallel processing of massive data sets. PVLDB 1(2), 1265\u20131276 (2008)","journal-title":"PVLDB"},{"issue":"3","key":"6_CR27","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s002360050120","volume":"35","author":"EYC Cheng","year":"1998","unstructured":"Cheng, E.Y.C., Kaminski, M.: Context-free languages over infinite alphabets. Acta Inf. 35(3), 245\u2013267 (1998)","journal-title":"Acta Inf."},{"key":"6_CR28","unstructured":"Chen, Y.-F., Lengal, O., Tan, T., Wu, Z.: Equivalence of streaming numerical transducers (2016). (manuscript)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-319-41540-6_6","volume-title":"Computer Aided Verification","author":"Y-F Chen","year":"2016","unstructured":"Chen, Y.-F., Song, L., Wu, Z.: The commutativity problem of the MapReduce framework: a transducer-based approach. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 91\u2013111. Springer, Cham (2016). doi:10.1007\/978-3-319-41540-6_6"},{"key":"6_CR30","unstructured":"D\u2019Antoni, L.: In the maze of data languages. CoRR, abs\/1208.5980 (2012)"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-319-08867-9_14","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2014","unstructured":"D\u2019Antoni, L., Alur, R.: Symbolic visibly pushdown automata. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 209\u2013225. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_14"},{"key":"6_CR32","unstructured":"Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. In: Proceedings of the 6th Symposium on Operating System Design and Implementation (OSDI), pp. 137\u2013150 (2004)"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-662-44584-6_34","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"N Decker","year":"2014","unstructured":"Decker, N., Habermehl, P., Leucker, M., Thoma, D.: Ordered navigation on multi-attributed data words. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 497\u2013511. Springer, Heidelberg (2014). doi:10.1007\/978-3-662-44584-6_34"},{"issue":"3","key":"6_CR34","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/1507244.1507246","volume":"10","author":"S Demri","year":"2009","unstructured":"Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3), 16:1\u201316:30 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006). doi:10.1007\/11691372_19"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 541\u2013554 (2014)","DOI":"10.1145\/2535838.2535849"},{"issue":"1","key":"6_CR37","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10703-015-0233-4","volume":"47","author":"L D\u2019Antoni","year":"2015","unstructured":"D\u2019Antoni, L., Veanes, M.: Extended symbolic finite automata and transducers. Form. Methods Syst. Des. 47(1), 93\u2013119 (2015)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR38","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1090\/S0002-9947-1961-0139530-9","volume":"98","author":"C Elgot","year":"1961","unstructured":"Elgot, C.: Decision problems of finite automata design and related arithmetic. Trans. Am. Math. Soc. 98, 21\u201352 (1961)","journal-title":"Trans. Am. Math. Soc."},{"key":"6_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-319-24953-7_7","volume-title":"Automated Technology for Verification and Analysis","author":"C Enea","year":"2015","unstructured":"Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 80\u201396. Springer, Cham (2015). doi:10.1007\/978-3-319-24953-7_7"},{"issue":"1","key":"6_CR40","first-page":"1","volume":"8","author":"D Figueira","year":"2012","unstructured":"Figueira, D.: Alternating register automata on finite words and trees. Log. Methods Comput. Sci. 8(1), 1\u201343 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"6_CR41","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-72248-6","volume-title":"Syntax-Directed Semantics - Formal Models Based on Tree Transducers","author":"Z F\u00fcl\u00f6p","year":"1998","unstructured":"F\u00fcl\u00f6p, Z., Vogler, H.: Syntax-Directed Semantics - Formal Models Based on Tree Transducers. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (1998)"},{"issue":"5","key":"6_CR42","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s00236-014-0197-7","volume":"51","author":"Z F\u00fcl\u00f6p","year":"2014","unstructured":"F\u00fcl\u00f6p, Z., Vogler, H.: Forward and backward application of symbolic tree transducers. Acta Inf. 51(5), 297\u2013325 (2014)","journal-title":"Acta Inf."},{"key":"6_CR43","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"JH Gallier","year":"1985","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers, Inc., New York (1985)"},{"key":"6_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-319-40229-1_36","volume-title":"Automated Reasoning","author":"X Gu","year":"2016","unstructured":"Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 532\u2013549. Springer, Cham (2016). doi:10.1007\/978-3-319-40229-1_36"},{"key":"6_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-642-13089-2_47","volume-title":"Language and Automata Theory and Applications","author":"O Grumberg","year":"2010","unstructured":"Grumberg, O., Kupferman, O., Sheinvald, S.: Variable automata over infinite alphabets. In: Dediu, A.-H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 561\u2013572. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-13089-2_47"},{"key":"6_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-33386-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"O Grumberg","year":"2012","unstructured":"Grumberg, O., Kupferman, O., Sheinvald, S.: Model checking systems and specifications with parameterized atomic propositions. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 122\u2013136. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33386-6_11"},{"key":"6_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-319-02444-8_28","volume-title":"Automated Technology for Verification and Analysis","author":"O Grumberg","year":"2013","unstructured":"Grumberg, O., Kupferman, O., Sheinvald, S.: An automata-theoretic approach to reasoning about parameterized systems and specifications. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 397\u2013411. Springer, Heidelberg (2013). doi:10.1007\/978-3-319-02444-8_28"},{"key":"6_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-319-11936-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"O Grumberg","year":"2014","unstructured":"Grumberg, O., Kupferman, O., Sheinvald, S.: A game-theoretic approach to simulation of data-parameterized systems. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 348\u2013363. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-11936-6_25"},{"issue":"3","key":"6_CR49","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":"1","key":"6_CR50","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-012-0150-8","volume":"41","author":"P Habermehl","year":"2012","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Form. Methods Syst. Des. 41(1), 83\u2013106 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-662-49630-5_26","volume-title":"Foundations of Software Science and Computation Structures","author":"P Hofman","year":"2016","unstructured":"Hofman, P., Lasota, S., Lazi\u0107, R., Leroux, J., Schmitz, S., Totzke, P.: Coverability trees for petri nets with unordered data. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 445\u2013461. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49630-5_26"},{"key":"6_CR52","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"6_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265\u2013281. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_19"},{"key":"6_CR54","unstructured":"Kara, A.: Logics on data words: expressivity, satisfiability, model checking. Ph.D. thesis, TU Dortmund University (2016). https:\/\/eldorado.tu-dortmund.de\/bitstream\/2003\/35216\/1\/Dissertation.pdf"},{"issue":"2","key":"6_CR55","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-28332-1_30","volume-title":"Language and Automata Theory and Applications","author":"A Kara","year":"2012","unstructured":"Kara, A., Schwentick, T., Tan, T.: Feasible automata for two-variable logic with successor on data words. In: Dediu, A.-H., Mart\u00edn-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 351\u2013362. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28332-1_30"},{"issue":"3","key":"6_CR57","doi-asserted-by":"publisher","first-page":"301","DOI":"10.3233\/FUN-2006-69304","volume":"69","author":"M Kaminski","year":"2006","unstructured":"Kaminski, M., Tan, T.: Regular expressions for languages over infinite alphabets. Fundam. Inform. 69(3), 301\u2013318 (2006)","journal-title":"Fundam. Inform."},{"issue":"4","key":"6_CR58","doi-asserted-by":"publisher","first-page":"379","DOI":"10.3233\/FI-2010-234","volume":"98","author":"M Kaminski","year":"2010","unstructured":"Kaminski, M., Tan, T.: A note on two-pebble automata over infinite alphabets. Fundam. Inform. 98(4), 379\u2013390 (2010)","journal-title":"Fundam. Inform."},{"key":"6_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-41528-4_21","volume-title":"Computer Aided Verification","author":"QL Le","year":"2016","unstructured":"Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382\u2013404. Springer, Cham (2016). doi:10.1007\/978-3-319-41528-4_21"},{"issue":"7","key":"6_CR60","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1016\/j.jcss.2015.03.005","volume":"81","author":"L Libkin","year":"2015","unstructured":"Libkin, L., Tan, T., Vrgoc, D.: Regular expressions for data words. J. Comput. Syst. Sci. 81(7), 1278\u20131297 (2015)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR61","volume-title":"Counter-Free Automata","author":"R McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S.: Counter-Free Automata. MIT Press, Cambridge (1971)"},{"key":"6_CR62","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 611\u2013622 (2011)","DOI":"10.1145\/1926385.1926455"},{"issue":"4","key":"6_CR63","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1142\/S0129054111008465","volume":"22","author":"A Manuel","year":"2011","unstructured":"Manuel, A., Ramanujam, R.: Class counting automata on datawords. Int. J. Found. Comput. Sci. 22(4), 863\u2013882 (2011)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"6_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-21493-6_16","volume-title":"Algebraic Informatics","author":"I-E Mens","year":"2011","unstructured":"Mens, I.-E., Rahonis, G.: Variable tree automata over infinite ranked alphabets. In: Winkler, F. (ed.) CAI 2011. LNCS, vol. 6742, pp. 247\u2013260. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-21493-6_16"},{"key":"6_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-662-44522-8_39","volume-title":"Mathematical Foundations of Computer Science 2014","author":"AS Murawski","year":"2014","unstructured":"Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: Reachability in pushdown register automata. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 464\u2013473. Springer, Heidelberg (2014). doi:10.1007\/978-3-662-44522-8_39"},{"key":"6_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1016","DOI":"10.1007\/978-3-540-27836-8_85","volume-title":"Automata, Languages and Programming","author":"M M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: A note on Karr\u2019s algorithm. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016\u20131028. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-27836-8_85"},{"issue":"2","key":"6_CR67","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR68","unstructured":"Neven, F., Schweikardt, N., Servais, F., Tan, T.: Distributed streaming with finite memory. In: Proceedings of the 18th International Conference on Database Theory (ICDT), pp. 324\u2013341 (2015)"},{"key":"6_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/3-540-44683-4_49","volume-title":"Mathematical Foundations of Computer Science 2001","author":"F Neven","year":"2001","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol. 2136, pp. 560\u2013572. Springer, Heidelberg (2001). doi:10.1007\/3-540-44683-4_49"},{"issue":"3","key":"6_CR70","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Log."},{"key":"6_CR71","doi-asserted-by":"crossref","unstructured":"Olston, C., Reed, B., Srivastava, U., Kumar, R., Tomkins, A.: Pig latin: a not-so-foreign language for data processing. In: Proceedings of the ACM SIGMOD International Conference on Management of Data (SIGMOD), pp. 1099\u20131110 (2008)","DOI":"10.1145\/1376616.1376726"},{"key":"6_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773\u2013789. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_54"},{"key":"6_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711\u2013728. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_47"},{"key":"6_CR74","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS), pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"6_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-319-46520-3_16","volume-title":"Automated Technology for Verification and Analysis","author":"A Reynolds","year":"2016","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 244\u2013261. Springer, Cham (2016). doi:10.1007\/978-3-319-46520-3_16"},{"issue":"2","key":"6_CR76","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1016\/S0019-9958(65)90108-7","volume":"8","author":"MP Sch\u00fctzenberger","year":"1965","unstructured":"Sch\u00fctzenberger, M.P.: On finite monoids having only trivial subgroups. Inf. Control 8(2), 190\u2013194 (1965)","journal-title":"Inf. Control"},{"key":"6_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/11874683_3","volume-title":"Computer Science Logic","author":"L Segoufin","year":"2006","unstructured":"Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41\u201357. Springer, Heidelberg (2006). doi:10.1007\/11874683_3"},{"key":"6_CR78","unstructured":"Sistla, A.P., German, S.M.: Reasoning with many processes. In: Proceedings of the 2nd Symposium on Logic in Computer Science (LICS), pp. 138\u2013152 (1987)"},{"issue":"3","key":"6_CR79","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR80","unstructured":"Song, F., Wu, Z.: Extending temporal logics with data variable quantifications. In: Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS), pp. 253\u2013265 (2014)"},{"key":"6_CR81","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.ic.2016.08.002","volume":"251","author":"F Song","year":"2016","unstructured":"Song, F., Zhilin, W.: On temporal logics with data variable quantifications: decidability and complexity. Inf. Comput. 251, 104\u2013139 (2016)","journal-title":"Inf. Comput."},{"issue":"8","key":"6_CR82","doi-asserted-by":"publisher","first-page":"778","DOI":"10.1016\/j.jcss.2010.03.004","volume":"76","author":"T Tan","year":"2010","unstructured":"Tan, T.: On pebble automata for data languages with decidable emptiness problem. J. Comput. Syst. Sci. 76(8), 778\u2013791 (2010)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"6_CR83","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2499937.2499940","volume":"14","author":"T Tan","year":"2013","unstructured":"Tan, T.: Graph reachability and pebble automata over infinite alphabets. ACM Trans. Comput. Log. 14(3), 19 (2013)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"6_CR84","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/2559945","volume":"15","author":"T Tan","year":"2014","unstructured":"Tan, T.: Extending two-variable logic on data trees with order on data values and its automata. ACM Trans. Comput. Log. 15(1), 8 (2014)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"6_CR85","first-page":"1626","volume":"2","author":"A Thusoo","year":"2009","unstructured":"Thusoo, A., Sarma, J.S., Jain, N., Shao, Z., Chakka, P., Anthony, S., Liu, H., Wyckoff, P., Murthy, R.: Hive - a warehousing solution over a map-reduce framework. PVLDB 2(2), 1626\u20131629 (2009)","journal-title":"PVLDB"},{"key":"6_CR86","first-page":"57","volume":"2","author":"JW Thatcher","year":"1968","unstructured":"Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Theory Comput. Syst. 2, 57\u201381 (1968)","journal-title":"Theory Comput. Syst."},{"key":"6_CR87","first-page":"141","volume":"105","author":"M Veanes","year":"2011","unstructured":"Veanes, M., Bj\u00f8rner, N.: Foundations of finite symbolic tree transducers. Bull. EATCS 105, 141\u2013173 (2011)","journal-title":"Bull. EATCS"},{"key":"6_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-29709-0_32","volume-title":"Perspectives of Systems Informatics","author":"M Veanes","year":"2012","unstructured":"Veanes, M., Bj\u00f8rner, N.: Symbolic tree transducers. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 377\u2013393. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-29709-0_32"},{"issue":"3","key":"6_CR89","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1016\/j.ipl.2014.11.005","volume":"115","author":"M Veanes","year":"2015","unstructured":"Veanes, M., Bj\u00f8rner, N.: Symbolic tree automata. Inf. Process. Lett. 115(3), 418\u2013424 (2015)","journal-title":"Inf. Process. Lett."},{"key":"6_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-319-41579-6_21","volume-title":"Perspectives of System Informatics","author":"M Veanes","year":"2016","unstructured":"Veanes, M., Bj\u00f8rner, N.: Equivalence of finite-valued symbolic finite transducers. In: Mazzara, M., Voronkov, A. (eds.) PSI 2015. LNCS, vol. 9609, pp. 276\u2013290. Springer, Cham (2016). doi:10.1007\/978-3-319-41579-6_21"},{"key":"6_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/978-3-319-08867-9_42","volume-title":"Computer Aided Verification","author":"M Veanes","year":"2014","unstructured":"Veanes, M., Bj\u00f8rner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 628\u2013645. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_42"},{"key":"6_CR92","doi-asserted-by":"crossref","unstructured":"Veanes, M., D\u2019Antoni, L.: Minimization of symbolic tree automata. In: Proceedings of the 30th IEEE Symposium on Logic in Computer Science (LICS) (2016)","DOI":"10.1145\/2933575.2933578"},{"key":"6_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-39274-0_3","volume-title":"Implementation and Application of Automata","author":"M Veanes","year":"2013","unstructured":"Veanes, M.: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 16\u201323. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39274-0_3"},{"key":"6_CR94","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bj\u00f8rner, N.: Symbolic finite state transducers: algorithms and applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 137\u2013150 (2012)","DOI":"10.1145\/2103656.2103674"},{"key":"6_CR95","doi-asserted-by":"crossref","unstructured":"Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: Proceedings of the 12th International Conference on Database Theory (ICDT), pp. 1\u201313 (2009)","DOI":"10.1145\/1514894.1514896"},{"key":"6_CR96","series-title":"Formal Models and Semantics, vol. B","volume-title":"Handbook of Theoretical Computer Science","year":"1990","unstructured":"van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B. Elsevier and MIT Press, Amsterdam and Cambridge (1990)"},{"issue":"3","key":"6_CR97","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1012291501330","volume":"4","author":"G van Noord","year":"2001","unstructured":"van Noord, G., Gerdemann, D.: Finite state transducers with predicates and identities. Grammars 4(3), 263\u2013286 (2001)","journal-title":"Grammars"},{"key":"6_CR98","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the 1st Symposium on Logic in Computer Science (LICS), pp. 332\u2013344 (1986)"},{"issue":"4","key":"6_CR99","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1017\/S135132499700154X","volume":"2","author":"BW Watson","year":"1996","unstructured":"Watson, B.W.: Implementing and using finite automata toolkits. Nat. Lang. Eng. 2(4), 295\u2013302 (1996)","journal-title":"Nat. Lang. Eng."},{"key":"6_CR100","unstructured":"Wu, Z.: A decidable extension of data automata. In: Proceedings of the 2nd International Symposium on Games, Automata, Logics and Formal Verification (GandALF), pp. 116\u2013130 (2011)"},{"key":"6_CR101","unstructured":"Wu, Z.: Commutative data automata. In: Proceedings of the 26th International Workshop, 21st Annual Conference on Computer Science Logic (CSL), pp. 528\u2013542 (2012)"},{"key":"6_CR102","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proceedings of the 24th Annual Symposium on Foundations of Computer Science (FOCS), pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"},{"key":"6_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/978-3-540-39910-0_33","volume-title":"Verification: Theory and Practice","author":"CG Zarba","year":"2003","unstructured":"Zarba, C.G.: Combining sets with elements. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 762\u2013782. Springer, Heidelberg (2003). doi:10.1007\/978-3-540-39910-0_33"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-56841-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T07:49:24Z","timestamp":1759996164000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-56841-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319568409","9783319568416"],"references-count":103,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-56841-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"6 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 March 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}