{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:23:10Z","timestamp":1777890190195,"version":"3.51.4"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633862","type":"print"},{"value":"9783319633879","type":"electronic"}],"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.springer.com\/tdm"},{"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.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_3","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"47-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":51,"title":["The Power of Symbolic Automata and Transducers"],"prefix":"10.1007","author":[{"given":"Loris","family":"D\u2019Antoni","sequence":"first","affiliation":[]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"3_CR1","unstructured":"AutomataDotNet. https:\/\/github.com\/AutomataDotNet\/"},{"key":"3_CR2","unstructured":"AutomatArk. https:\/\/github.com\/lorisdanto\/automatark"},{"key":"3_CR3","unstructured":"Symbolic Automata. http:\/\/pages.cs.wisc.edu\/~loris\/symbolicautomata.html"},{"key":"3_CR4","unstructured":"symbolicautomata. https:\/\/github.com\/lorisdanto\/symbolicautomata\/"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11605157_3","volume-title":"Implementation and Application of Automata","author":"PA Abdulla","year":"2006","unstructured":"Abdulla, P.A., Deneux, J., Kaati, L., Nilsson, M.: Minimization of non-deterministic automata with large alphabets. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 31\u201342. Springer, Heidelberg (2006). doi:10.1007\/11605157_3"},{"issue":"6","key":"3_CR6","doi-asserted-by":"publisher","first-page":"983","DOI":"10.1142\/S0129054103002126","volume":"14","author":"C Allauzen","year":"2003","unstructured":"Allauzen, C., Mohri, M.: Finitely subsequential transducers. Int. J. Found. Compu. Sci. 14(6), 983\u2013994 (2003)","journal-title":"Int. J. Found. Compu. Sci."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., D\u2019Antoni, L., Raghothaman, M.: Drex: a declarative language for efficiently evaluating regular string transformations. In: ACM SIGPLAN Notices - POPL 2015, vol. 50, no. 1, pp. 125\u2013137 (2015)","DOI":"10.1145\/2775051.2676981"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Argyros, G., Stais, I., Kiayias, A., Keromytis, A.D.: Back in black: towards formal, black box analysis of sanitizers and filters. In: 2016 IEEE Symposium on Security and Privacy (SP), pp. 91\u2013109 (2016)","DOI":"10.1109\/SP.2016.14"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-15205-4_12","volume-title":"Computer Science Logic","author":"M Benedikt","year":"2010","unstructured":"Benedikt, M., Ley, C., Puppis, G.: Automata vs. logics on data words. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 110\u2013124. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-15205-4_12"},{"key":"3_CR10","unstructured":"Bj\u00f8rner, N., Ganesh, V., Michel, R., Veanes, M.: An SMT-LIB format for sequences and regular expressions. In: SMT Workshop (2012)"},{"issue":"1","key":"3_CR11","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2490818","volume":"15","author":"F Bonchi","year":"2014","unstructured":"Bonchi, F., Bonsangue, M.M., Hansen, H.H., Panangaden, P., Rutten, J.J.M.M., Silva, A.: Algebra-coalgebra duality in Brzozowski\u2019s minimization algorithm. ACM Trans. Comput. Logic 15(1), 3:1\u20133:29 (2014)","journal-title":"ACM Trans. Comput. Logic"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Botin\u010dan, M., Babi\u0107, D.: Sigma*: symbolic learning of input-output specifications. In: ACM SIGPLAN Notices - POPL 2013, vol. 48, no. 1, pp. 443\u2013456 (2013)","DOI":"10.1145\/2480359.2429123"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372\u2013386. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-27813-9_29"},{"issue":"1","key":"3_CR14","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Dalla Preda, M., Giacobazzi, R., Lakhotia, A., Mastroeni, I.: Abstract symbolic automata: mixed syntactic\/semantic similarity analysis of executables. In: ACM SIGPLAN Notices - POPL 2015, vol. 50, no. 1, pp. 329\u2013341 (2015)","DOI":"10.1145\/2775051.2676986"},{"key":"3_CR16","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":"3_CR17","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Kincaid, Z., Wang, F.: A symbolic decision procedure for symbolic alternating finite automata. In: MFPS 2017 (2017)","DOI":"10.1016\/j.entcs.2018.03.017"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: ACM SIGPLAN Notices - POPL 2014, vol. 49, no. 1, pp. 541\u2013553 (2014)","DOI":"10.1145\/2578855.2535849"},{"issue":"1","key":"3_CR19","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":"3_CR20","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic tree automata. In: LICS 2016, pp. 873\u2013882. ACM, New York (2016)","DOI":"10.1145\/2933575.2933578"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-662-54577-5_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L D\u2019Antoni","year":"2017","unstructured":"D\u2019Antoni, L., Veanes, M.: Forward bisimulations for nondeterministic symbolic finite automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 518\u2013534. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54577-5_30"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Monadic second-order logic on finite sequences. In: ACM SIGPLAN Notices - POPL\u201917, vol. 52, no. 1, pp. 232\u2013245 (2017)","DOI":"10.1145\/3093333.3009844"},{"issue":"1","key":"3_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2791292","volume":"38","author":"L D\u2019Antoni","year":"2015","unstructured":"D\u2019Antoni, L., Veanes, M., Livshits, B., Molnar, D.: Fast: a transducer-based language for tree manipulation. ACM TOPLAS 38(1), 1\u201332 (2015)","journal-title":"ACM TOPLAS"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-662-54577-5_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Drews","year":"2017","unstructured":"Drews, S., D\u2019Antoni, L.: Learning symbolic automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 173\u2013189. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54577-5_10"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. ACM SIGPLAN Notices - POPL 2002, 37(1), 191\u2013202 (2002)","DOI":"10.1145\/565816.503291"},{"issue":"4","key":"3_CR27","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0020-0190(93)90143-W","volume":"48","author":"Z F\u00fcl\u00f6p","year":"1993","unstructured":"F\u00fcl\u00f6p, Z., Gyenizse, P.: On injectivity of deterministic top-down tree transducers. Inf. Process. Lett. 48(4), 183\u2013188 (1993)","journal-title":"Inf. Process. Lett."},{"issue":"5","key":"3_CR28","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 Informatica 51(5), 297\u2013325 (2014)","journal-title":"Acta Informatica"},{"key":"3_CR29","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1145\/321466.321473","volume":"15","author":"T Griffiths","year":"1968","unstructured":"Griffiths, T.: The unsolvability of the equivalence problem for $$\\varLambda $$-free nondeterministic generalized machines. J. ACM 15, 409\u2013413 (1968)","journal-title":"J. ACM"},{"key":"3_CR30","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with BEK. In: Proceedings of the 20th USENIX Conference on Security, SEC 2011, Berkeley, CA, USA, p. 1. USENIX Association (2011)"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-18275-4_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Hooimeijer","year":"2011","unstructured":"Hooimeijer, P., Veanes, M.: An evaluation of automata algorithms for string analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 248\u2013262. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-18275-4_18"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An $$n$$log$$n$$ algorithm for minimizing states in a finite automaton. In: Kohavi, Z. (ed.) Theory of Machines and Computations (Proceedings of International Symposium Technion, Haifa), pp. 189\u2013196 (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Hu, Q., D\u2019Antoni, L.: Automatic program inversion using symbolic transducers. In: ACM SIGPLAN Notices - PLDI 2017 (2017, to appear)","DOI":"10.1145\/3062341.3062345"},{"key":"3_CR34","unstructured":"Keil, M., Thiemann, P.: Symbolic solving of extended regular expression inequalities. In: FSTTCS 2014, LIPIcs, pp. 175\u2013186 (2014)"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_43"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Mamouras, K., Raghotaman, M., Alur, R., Ives, Z.G., Khanna, S.: StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming data. In: ACM SIGPLAN Notices - PLDI 2017 (2017, to appear)","DOI":"10.1145\/3062341.3062369"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: ACM SIGPLAN Notices - POPL 2017, vol. 52, no. 1, pp. 613\u2013625 (2017)","DOI":"10.1145\/3093333.3009879"},{"issue":"2","key":"3_CR38","first-page":"269","volume":"23","author":"M Mohri","year":"1997","unstructured":"Mohri, M.: Finite-state transducers in language and speech processing. Comput. Linguist. 23(2), 269\u2013311 (1997)","journal-title":"Comput. Linguist."},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Mytkowicz, T., Musuvathi, M., Schulte, W.: Data-parallel finite-state machines. In: ACM SIGPLAN Notices - ASPLOS 2014, vol. 49, no. 4, pp. 529\u2013542 (2014)","DOI":"10.1145\/2644865.2541988"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Ohmann, P., Brooks, A., D\u2019Antoni, L., Liblit, B.: Control-flow recovery from partial failure reports. In: ACM SIGPLAN Notices - PLDI 2017 (2017, to appear)","DOI":"10.1145\/3062341.3062368"},{"issue":"6","key":"3_CR41","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"key":"3_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-662-53413-7_7","volume-title":"Static Analysis","author":"M Dalla Preda","year":"2016","unstructured":"Dalla Preda, M., Giacobazzi, R., Mastroeni, I.: Completeness in approximate transduction. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 126\u2013146. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-53413-7_7"},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417\u2013431. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-21437-0_31"},{"key":"3_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/978-3-319-63390-9_10","volume-title":"CAV 2017","author":"O Saarikivi","year":"2017","unstructured":"Saarikivi, O., Veanes, M.: Minimization of symbolic transducers. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 176\u2013196. Springer, Cham (2017)"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Saarikivi, O., Veanes, M., Mytkowicz, T., Musuvathi, M.: Fusing effectful comprehensions. In: ACM SIGPLAN Notices - PLDI 2017. ACM (2017, to appear)","DOI":"10.1145\/3062341.3062362"},{"key":"3_CR46","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0304-3975(77)90055-X","volume":"4","author":"MP Sch\u00fctzenberger","year":"1977","unstructured":"Sch\u00fctzenberger, M.P.: Sur une variante des fonctions s\u00e9quentielles. Theoret. Comput. Sci. 4, 47\u201357 (1977)","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR47","doi-asserted-by":"crossref","unstructured":"Stearns, R.E., Hunt, H.B.: On the equivalence and containment problems for unambiguous regular expressions, grammars, and automata. In: SFCS 1981, pp. 74\u201381, October 1981","DOI":"10.1109\/SFCS.1981.29"},{"key":"3_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N Tillmann","year":"2008","unstructured":"Tillmann, N., Halleux, J.: Pex\u2013white box test generation for\u00a0.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134\u2013153. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-79124-9_10"},{"issue":"3","key":"3_CR49","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":"3_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-662-46823-4_27","volume-title":"Perspectives of System Informatics","author":"M Veanes","year":"2015","unstructured":"Veanes, M.: Symbolic string transformations with regular lookahead and rollback. In: Voronkov, A., Virbitskaite, I. (eds.) PSI 2014. LNCS, vol. 8974, pp. 335\u2013350. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46823-4_27"},{"key":"3_CR51","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":"3_CR52","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. Informat. Process. Lett. 115(3), 418\u2013424 (2015)","journal-title":"Informat. Process. Lett."},{"key":"3_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-16242-8_45","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Veanes","year":"2010","unstructured":"Veanes, M., Bj\u00f8rner, N., Moura, L.: Symbolic automata constraint solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 640\u2013654. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-16242-8_45"},{"issue":"2","key":"3_CR54","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/3040488","volume":"64","author":"M Veanes","year":"2017","unstructured":"Veanes, M., Bj\u00f8rner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. J. ACM 64(2), 14:1\u201314:28 (2017)","journal-title":"J. ACM"},{"key":"3_CR55","doi-asserted-by":"crossref","unstructured":"Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: ICST 2010, pp. 498\u2013507. IEEE (2010)","DOI":"10.1109\/ICST.2010.15"},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-10373-5_3","volume-title":"Formal Methods and Software Engineering","author":"M Veanes","year":"2009","unstructured":"Veanes, M., Grigorenko, P., de Halleux, P., Tillmann, N.: Symbolic query exploration. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 49\u201368. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-10373-5_3"},{"key":"3_CR57","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bj\u00f8rner, N.: Symbolic finite state transducers: algorithms and applications. In: ACM SIGPLAN Notices - POPL 2012, vol. 47, no. 1, pp. 137\u2013150 (2012)","DOI":"10.1145\/2103621.2103674"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Veanes, M., Mytkowicz, T., Molnar, D., Livshits, B.: Data-parallel string-manipulating programs. In: ACM SIGPLAN Notices - POPL 2015, vol. 50, no. 1, pp. 139\u2013152 (2015)","DOI":"10.1145\/2775051.2677014"},{"key":"3_CR59","unstructured":"Watson, B.W.: Implementing and using finite automata toolkits. In: Extended Finite State Models of Language, pp. 19\u201336. Cambridge University Press (1999)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T20:24:32Z","timestamp":1659212672000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}