Reasoning About Vectors Using an SMT Theory of Sequences

Ying Sheng; Andres Notzli; Andrew Reynolds; Yoni Zohar; David Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark Barrett; Cesare Tinelli

doi:10.1007/978-3-031-10769-6_9

Back

Reasoning About Vectors Using an SMT Theory of Sequences

Conference proceeding

Open access

Peer reviewed

Reasoning About Vectors Using an SMT Theory of Sequences

Ying Sheng, Andres Notzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett and Cesare Tinelli

AUTOMATED REASONING, IJCAR 2022, Vol.13385, pp.125-143

Lecture Notes in Artificial Intelligence

01/01/2022

DOI: 10.1007/978-3-031-10769-6_9

Files and links (1)

url

https://doi.org/10.1007/978-3-031-10769-6_9View

Published (Version of record) Open Access

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.

Computer Science

Logic

Mathematics

Physical Sciences

Technology

Computer Science, Artificial Intelligence

Computer Science, Theory & Methods

Mathematics, Applied

Science & Technology

Science & Technology - Other Topics

Details

Title: Subtitle: Reasoning About Vectors Using an SMT Theory of Sequences
Creators: Ying Sheng - Stanford University
Andres Notzli - Stanford University
Andrew Reynolds - University of Iowa
Yoni Zohar - Bar-Ilan University
David Dill - Menlo School
Wolfgang Grieskamp - Menlo School
Junkil Park - Menlo School
Shaz Qadeer - Menlo School
Clark Barrett - Stanford University
Cesare Tinelli - University of Iowa
Contributors: J Blanchette (Editor)
L Kovacs (Editor)
D Pattinson (Editor)
Resource Type: Conference proceeding
Publication Details: AUTOMATED REASONING, IJCAR 2022, Vol.13385, pp.125-143
Series: Lecture Notes in Artificial Intelligence
DOI: 10.1007/978-3-031-10769-6_9
ISSN: 0302-9743
eISSN: 1611-3349
Publisher: Springer Nature
Number of pages: 19
Grant note: Meta Novi 2110397; 2020704 / Stanford Center for Blockchain Research, NSF-BSF
Language: English
Date published: 01/01/2022
Academic Unit: Computer Science
Record Identifier: 9984410857002771

Metrics

36 Record Views

6 Times Cited - Web of Science