Abstract
Constraints over regular and context-free languages are common in the context of string-manipulating programs. Efficient solving of such constraints, often in combination with arithmetic and other theories, has many useful applications in program analysis and testing. We introduce and evaluate a method for symbolically expressing and solving constraints over automata, including subset constraints. Our method uses techniques present in the state-of-the-art SMT solver Z3.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
BRICS finite state automata utilities, http://www.brics.dk/automaton/
Axelsson, R., Heljanko, K., Lange, M.: Analyzing context-free grammars using an incremental SAT solver. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 410–422. Springer, Heidelberg (2008)
Blum, N., Koch, R.: Greibach Normal Form Transformation Revisited. Inf. Comput. 150(1), 112–118 (1999)
Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: DAC 1990, pp. 40–45. ACM, New York (1990)
Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise Analysis of String Expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1–18. Springer, Heidelberg (2003)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. TACAS 2008, pp. 337–340. Springer, Heidelberg (2008)
Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)
Hodges, W.: Model theory. Cambridge Univ. Press, Cambridge (1995)
Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: PLDI, pp. 188–198 (2009)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: ISSTA 2009, pp. 105–116. ACM, New York (2009)
Klarlund, N.: Mona & Fido: The Logic-Automaton Connection in Practice. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 311–326. Springer, Heidelberg (1998)
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)
MSDN. .NET Framework Regular Expressions (2009), http://msdn.microsoft.com/en-us/library/hs600312.aspx
Schmitz, S.: Conservative ambiguity detection in context-free grammars. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 692–703. Springer, Heidelberg (2007)
Shannon, D., Hajra, S., Lee, A., Zhan, D., Khurshid, S.: Abstracting Symbolic Execution with String Analysis. In: MUTATION 2007, pp. 13–22. IEEE, Los Alamitos (2007)
Veanes, M., Bjørner, N., de Moura, L.: Solving extended regular constraints symbolically. Technical Report MSR-TR-2009-177, Microsoft Research (2009)
Veanes, M., de Halleux, P., Tillmann, N.: Rex: Symbolic Regular Expression Explorer. In: ICST 2010, IEEE, Los Alamitos (2010)
Veanes, M., Tillmann, N., de Halleux, J.: Qex: Symbolic SQL query explorer. In: LPAR-16. LNCS (LNAI). Springer, Heidelberg (2010)
Wassermann, G., Gould, C., Su, Z., Devanbu, P.: Static checking of dynamically generated queries in database applications. ACM TSEM 16(4), 14 (2007)
Watson, B.W.: chapter Implementing and using finite automata toolkits, pp. 19–36. Cambridge U. Press, Cambridge (1999)
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. 5156, pp. 306–324. Springer, Heidelberg (2008)
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. 5505, pp. 322–336. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Veanes, M., Bjørner, N., de Moura, L. (2010). Symbolic Automata Constraint Solving. In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_45
Download citation
DOI: https://doi.org/10.1007/978-3-642-16242-8_45
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16241-1
Online ISBN: 978-3-642-16242-8
eBook Packages: Computer ScienceComputer Science (R0)