A Solver for Arrays with Concatenation

Abdulla, P.A., Atig, M.F., Chen, Y.-F., Holík, L., Rezine, A., Rümmer, P., Stenman, J.: String constraints for verification. In: International Conference on Computer Aided Verification, pp. 150–166. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_10

Abdulla, P.A., Atig, M.F., Diep, B.P., Holík, L., Janků, P.: Chain-free string constraints. In: International Symposium on Automated Technology for Verification and Analysis, pp. 277–293. Springer (2019). https://doi.org/10.1007/978-3-030-31784-3_16

Appel, A.W.: Verified software toolchain. In: European Symposium on Programming, pp. 1–17. Springer (2011). https://doi.org/10.1007/978-3-642-19718-5_1

Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305–343. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_11

Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside coq. In: International Conference on Certified Programs and Proofs, pp. 151–166. Springer (2011). https://doi.org/10.1007/978-3-642-25379-9_13

Bjørner, N., Ganesh, V., Michel, R., Veanes, M.: An SMT-LIB format for sequences and regular expressions. SMT 12, 76–86 (2012)

Bradley, A.R., Manna, Z., Sipma,H.B.: What’s decidable about arrays? In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 427–442. Springer (2006). https://doi.org/10.1007/11609773_28

Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1–4), 367–422 (2018). https://doi.org/10.1007/s10817-018-9457-5

Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z..: What is decidable about string constraints with the replaceall function. In: Proceedings of the ACM on Programming Languages, 2(POPL):1–29 (2017). https://doi.org/10.1145/3158091

Daca, P., Henzinger, T.A., Kupriyanov, A.: Array folds logic. In: International Conference on Computer Aided Verification, pp. 230–248. Springer (2016). https://doi.org/10.1007/978-3-319-41540-6_13

Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what’s decidable? In: Haifa Verification Conference, pp. 209–226. Springer (2012). https://doi.org/10.1007/978-3-642-39611-3_21

Ge, Y., De Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: International Conference on Computer Aided Verification, pp. 306–320. Springer (2009). https://doi.org/10.1007/978-3-642-02658-4_25

Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: International Conference on Foundations of Software Science and Computational Structures, pp. 474–489. Springer (2008). https://doi.org/10.1007/978-3-540-78499-9_33

Holík, L., Janků, P., Lin, A.W., Rümmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. In: Proceedings of the ACM on Programming Languages 2(POPL), pp. 1–32 (2017). https://doi.org/10.1145/3158092

Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for C and Java. In: NASA Formal Methods Symposium, pp. 41–55. Springer (2011). https://doi.org/10.1007/978-3-642-20398-5_4

Leino, K., Rustan, M.: Dafny: An automatic program verifier for functional correctness. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 348–370. Springer (2010). https://doi.org/10.1007/978-3-642-17511-4_20

Lin, A.W., Barceló, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 123–136 (2016). https://doi.org/10.1145/2837614.2837641

Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 145(2), 147–236 (1977)

McCarthy, J.: Towards a mathematical science of computation. In: Program Verification, pp. 35–56. Springer (1993). https://doi.org/10.1007/978-94-011-1793-7_2

Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc, Hoboken (1967)

Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM 51(3), 483–496 (2004). https://doi.org/10.1145/990308.990312

Plandowski, W.: An efficient algorithm for solving word equations. In: Proceedings of the Thirty-Eighth Annual ACM Symposium on Theory of Computing, pp. 467–476. ACM (2006). https://doi.org/10.1145/1132516.1132584

Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 29–37. IEEE (2001)

Zaostrovnykh, A., Pirelli, S., Pedrosa, L., Argyraki, K., Candea, G.: A formally verified NAT. In: Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM’17), pp. 141–154 (2017)

Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Berzish, M., Dolby, J., Zhang, X.: Z3str2: an efficient solver for strings, regular expressions, and length constraints. Formal Methods System Des 50(2–3), 249–288 (2017). https://doi.org/10.1007/s10703-016-0263-6