Journal article
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences
Journal of automated reasoning, Vol.67(3), 32
09/01/2023
DOI: 10.1007/s10817-023-09682-2
Abstract
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.
Details
- Title: Subtitle
- Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences
- Creators
- Ying Sheng - Stanford UniversityAndres Nötzli - Stanford UniversityAndrew Reynolds - University of IowaYoni Zohar - Bar-Ilan UniversityDavid Dill - Meta NoviWolfgang Grieskamp - Meta NoviJunkil Park - Meta NoviShaz Qadeer - Meta NoviClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Journal of automated reasoning, Vol.67(3), 32
- Publisher
- Springer Netherlands
- DOI
- 10.1007/s10817-023-09682-2
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- Grant note
- Stanford Center for Blockchain Research 2020704 / BSF Meta Novi 2110397 / NSF 619/21 / ISF
- Language
- English
- Date published
- 09/01/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984464517102771
Metrics
3 Record Views