“Reasoning About Vectors Using an SMT Theory of Sequences” by Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett, and Cesare Tinelli. In Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), (Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, eds.), Aug. 2022, pp. 125-143.
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.
BibTeX entry:
@inproceedings{SNR+22,
author = {Ying Sheng and Andres N{\"o}tzli and Andrew Reynolds and Yoni
Zohar and David Dill and Wolfgang Grieskamp and Junkil Park and
Shaz Qadeer and Clark Barrett and Cesare Tinelli},
editor = {Jasmin Blanchette and Laura Kov{\'a}cs and Dirk Pattinson},
title = {Reasoning About Vectors Using an SMT Theory of Sequences},
booktitle = {Proceedings of the {\it 11^{th}} International Joint
Conference on Automated Reasoning (IJCAR '22)},
series = {Lecture Notes in Computer Science},
volume = {13385},
pages = {125--143},
publisher = {Springer Nature},
month = aug,
year = {2022},
doi = {10.1007/978-3-031-10769-6_7},
url = {http://theory.stanford.edu/~barrett/pubs/SNR+22.pdf}
}
(This webpage was created with bibtex2web.)