Reasoning about vectors using an SMT theory of sequences. (English) Zbl 07628185
Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 125-143 (2022).
Summary: Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because the number of elements is fixed (determined by its index sort) and cannot be adjusted, which is a problem, given that the length of vectors often plays an important role when reasoning about vector programs. In this paper, we propose reasoning about vectors using a theory of sequences. We introduce the theory, propose a basic calculus adapted from one for the theory of strings, and extend it to efficiently handle common vector operations. We prove that our calculus is sound and show how to construct a model when it terminates with a saturated configuration. Finally, we describe an implementation of the calculus in cvc5 and demonstrate its efficacy by evaluating it on verification conditions for smart contracts and benchmarks derived from existing array benchmarks.
For the entire collection see [Zbl 1499.68012].
For the entire collection see [Zbl 1499.68012].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Alberti, F.; Ghilardi, S.; Pagani, E., Cardinality constraints for arrays (decidability results and applications), Formal Methods Syst. Des., 51, 3, 545-574 (2017) · Zbl 1377.68125 · doi:10.1007/s10703-017-0279-6 |
| [2] | Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415-442. Springer, Cham (2022). doi:10.1007/978-3-030-99524-9_24 |
| [3] | Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org |
| [4] | Barrett, C.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C.; Hermann, M.; Voronkov, A., Splitting on demand in SAT modulo theories, Logic for Programming, Artificial Intelligence, and Reasoning, 512-526 (2006), Heidelberg: Springer, Heidelberg · Zbl 1165.68480 · doi:10.1007/11916277_35 |
| [5] | Barrett, C.; Tinelli, C.; Clarke, E.; Henzinger, T.; Veith, H.; Bloem, R., Satisfiability modulo theories, Handbook of Model Checking, 305-343 (2018), Cham: Springer, Cham · Zbl 1392.68379 · doi:10.1007/978-3-319-10575-8_11 |
| [6] | Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2-6 October 2017, pp. 55-59. IEEE (2017) |
| [7] | Bjørner, N., de Moura, L., Nachmanson, L., Wintersteiger, C.: Programming Z3 (2018). https://theory.stanford.edu/ nikolaj/programmingz3.html#sec-sequences-and-strings |
| [8] | Bjørner, N.; Ganesh, V.; Michel, R.; Veanes, M., An SMT-LIB format for sequences and regular expressions, SMT, 12, 76-86 (2012) |
| [9] | Bjørner, N.; Tillmann, N.; Voronkov, A.; Kowalewski, S.; Philippou, A., Path feasibility analysis for string-manipulating programs, Tools and Algorithms for the Construction and Analysis of Systems, 307-321 (2009), Heidelberg: Springer, Heidelberg · Zbl 1234.68070 · doi:10.1007/978-3-642-00768-2_27 |
| [10] | Christ, J.; Hoenicke, J.; Lutz, C.; Ranise, S., Weakly equivalent arrays, Frontiers of Combining Systems, 119-134 (2015), Cham: Springer, Cham · Zbl 1471.68136 · doi:10.1007/978-3-319-24246-0_8 |
| [11] | de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [12] | Elad, N.; Rain, S.; Immerman, N.; Kovács, L.; Sagiv, M.; Silva, A.; Leino, KRM, Summing up smart transitions, Computer Aided Verification, 317-340 (2021), Cham: Springer, Cham · doi:10.1007/978-3-030-81685-8_15 |
| [13] | Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press (2001) · Zbl 0992.03001 |
| [14] | Falke, S.; Merz, F.; Sinz, C.; Cohen, E.; Rybalchenko, A., Extending the theory of arrays: memset, memcpy, and beyond, Verified Software: Theories, Tools, Experiments, 108-128 (2014), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-54108-7_6 |
| [15] | Ganesh, V.; Minnes, M.; Solar-Lezama, A.; Rinard, M.; Biere, A.; Nahir, A.; Vos, T., Word equations with length constraints: what’s decidable?, Hardware and Software: Verification and Testing, 209-226 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39611-3_21 |
| [16] | Jovanović, D.; Barrett, C.; Fermüller, CG; Voronkov, A., Polite theories revisited, Logic for Programming, Artificial Intelligence, and Reasoning, 402-416 (2010), Heidelberg: Springer, Heidelberg · Zbl 1306.68147 · doi:10.1007/978-3-642-16242-8_29 |
| [17] | Liang, T.; Reynolds, A.; Tinelli, C.; Barrett, C.; Deters, M.; Biere, A.; Bloem, R., A DPLL(T) theory solver for a theory of strings and regular expressions, Computer Aided Verification, 646-662 (2014), Cham: Springer, Cham · doi:10.1007/978-3-319-08867-9_43 |
| [18] | Nelson, G.; Oppen, DC, Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 2, 245-257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079 |
| [19] | Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J. ACM, 53, 6, 937-977 (2006) · Zbl 1326.68164 · doi:10.1145/1217856.1217859 |
| [20] | Ranise, S.; Ringeissen, C.; Zarba, CG; Gramlich, B., Combining data structures with nonstably infinite theories using many-sorted logic, Frontiers of Combining Systems, 48-64 (2005), Heidelberg: Springer, Heidelberg · Zbl 1171.68439 · doi:10.1007/11559306_3 |
| [21] | Reynolds, A., Nötzli, A., Barrett, C.W., Tinelli, C.: Reductions for strings and regular expressions revisited. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21-24 September 2020, pp. 225-235. IEEE (2020) |
| [22] | Reynolds, A.; Woo, M.; Barrett, C.; Brumley, D.; Liang, T.; Tinelli, C.; Majumdar, R.; Kunčak, V., Scaling up DPLL(T) string solvers using context-dependent simplification, Computer Aided Verification, 453-474 (2017), Cham: Springer, Cham · Zbl 1494.68255 · doi:10.1007/978-3-319-63390-9_24 |
| [23] | Sheng, Y.,et al.: Reasoning about vectors using an SMT theory of sequences. CoRR 10.48550/ARXIV.2205.08095 (2022) |
| [24] | Zhong, JE; Lahiri, SK; Wang, C., The move prover, Computer Aided Verification, 137-150 (2020), Cham: Springer, Cham · doi:10.1007/978-3-030-53288-8_7 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
