{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:28Z","timestamp":1767927808629,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642162411","type":"print"},{"value":"9783642162428","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_45","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T08:51:59Z","timestamp":1286182319000},"page":"640-654","source":"Crossref","is-referenced-by-count":21,"title":["Symbolic Automata Constraint Solving"],"prefix":"10.1007","author":[{"given":"Margus","family":"Veanes","sequence":"first","affiliation":[]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"45_CR1","unstructured":"BRICS finite state automata utilities, http:\/\/www.brics.dk\/automaton\/"},{"key":"45_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-70583-3_34","volume-title":"Automata, Languages and Programming","author":"R. Axelsson","year":"2008","unstructured":"Axelsson, R., Heljanko, K., Lange, M.: Analyzing context-free grammars using an incremental SAT solver. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 410\u2013422. Springer, Heidelberg (2008)"},{"issue":"1","key":"45_CR3","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1006\/inco.1998.2772","volume":"150","author":"N. Blum","year":"1999","unstructured":"Blum, N., Koch, R.: Greibach Normal Form Transformation Revisited. Inf. Comput.\u00a0150(1), 112\u2013118 (1999)","journal-title":"Inf. Comput."},{"key":"45_CR4","first-page":"40","volume-title":"DAC 1990","author":"K.S. Brace","year":"1990","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: DAC 1990, pp. 40\u201345. ACM, New York (1990)"},{"key":"45_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"A.S. Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise Analysis of String Expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 1\u201318. Springer, Heidelberg (2003)"},{"key":"45_CR6","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 de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a0TACAS 2008, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"45_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"45_CR8","volume-title":"Model theory","author":"W. Hodges","year":"1995","unstructured":"Hodges, W.: Model theory. Cambridge Univ. Press, Cambridge (1995)"},{"key":"45_CR9","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: PLDI, pp. 188\u2013198 (2009)","DOI":"10.1145\/1542476.1542498"},{"key":"45_CR10","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"45_CR11","first-page":"105","volume-title":"ISSTA 2009","author":"A. Kiezun","year":"2009","unstructured":"Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: ISSTA 2009, pp. 105\u2013116. ACM, New York (2009)"},{"key":"45_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BFb0028022","volume-title":"Computer Science Logic","author":"N. Klarlund","year":"1998","unstructured":"Klarlund, N.: Mona & Fido: The Logic-Automaton Connection in Practice. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol.\u00a01414, pp. 311\u2013326. Springer, Heidelberg (1998)"},{"key":"45_CR13","doi-asserted-by":"crossref","unstructured":"Li, N., Xie, T., Tillmann, N., de Halleux, P., Schulte, W.: Reggae: Automated test generation for programs using complex regular expressions. In: ASE 2009 (2009)","DOI":"10.1109\/ASE.2009.67"},{"key":"45_CR14","unstructured":"MSDN. .NET Framework Regular Expressions (2009), http:\/\/msdn.microsoft.com\/en-us\/library\/hs600312.aspx"},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"Schmitz, S.: Conservative ambiguity detection in context-free grammars. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol.\u00a04596, pp. 692\u2013703. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73420-8_60"},{"key":"45_CR16","first-page":"13","volume-title":"MUTATION 2007","author":"D. Shannon","year":"2007","unstructured":"Shannon, D., Hajra, S., Lee, A., Zhan, D., Khurshid, S.: Abstracting Symbolic Execution with String Analysis. In: MUTATION 2007, pp. 13\u201322. IEEE, Los Alamitos (2007)"},{"key":"45_CR17","unstructured":"Veanes, M., Bj\u00f8rner, N., de Moura, L.: Solving extended regular constraints symbolically. Technical Report MSR-TR-2009-177, Microsoft Research (2009)"},{"key":"45_CR18","volume-title":"ICST 2010","author":"M. Veanes","year":"2010","unstructured":"Veanes, M., de Halleux, P., Tillmann, N.: Rex: Symbolic Regular Expression Explorer. In: ICST 2010, IEEE, Los Alamitos (2010)"},{"key":"45_CR19","doi-asserted-by":"crossref","unstructured":"Veanes, M., Tillmann, N., de Halleux, J.: Qex: Symbolic SQL query explorer. In: LPAR-16. LNCS (LNAI). Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-17511-4_24"},{"issue":"4","key":"45_CR20","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1276933.1276935","volume":"16","author":"G. Wassermann","year":"2007","unstructured":"Wassermann, G., Gould, C., Su, Z., Devanbu, P.: Static checking of dynamically generated queries in database applications. ACM TSEM\u00a016(4), 14 (2007)","journal-title":"ACM TSEM"},{"key":"45_CR21","first-page":"19","volume-title":"chapter Implementing and using finite automata toolkits","author":"B.W. Watson","year":"1999","unstructured":"Watson, B.W.: chapter Implementing and using finite automata toolkits, pp. 19\u201336. Cambridge U. Press, Cambridge (1999)"},{"key":"45_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-85114-1_21","volume-title":"Model Checking Software","author":"F. Yu","year":"2008","unstructured":"Yu, F., Bultan, T., Cova, M., Ibarra, O.H.: Symbolic String Verification: An Automata-Based Approach. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 306\u2013324. Springer, Heidelberg (2008)"},{"key":"45_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/978-3-642-00768-2_28","volume-title":"TACAS 2009","author":"F. Yu","year":"2009","unstructured":"Yu, F., Bultan, T., Ibarra, O.H.: Symbolic String Verification: Combining String Analysis and Size Analysis. In: Kowlaewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 322\u2013336. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_45","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T02:02:20Z","timestamp":1559700140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}