More Like this

1. Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences

   https://doi.org/10.1007/s10817-023-09682-2  

   Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (September 2023, Journal of Automated Reasoning)

   Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (Ed.)

   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. 

   more » « less
2. Reasoning About Vectors Using an SMT Theory of Sequences

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

   Sheng, Ying; Noetzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (July 2022, International Joint Conference on Automated Reasoning (IJCAR))

   Blanchette, Jasmin; Kovacs, Laura; Pattinson, Dirk (Ed.)

   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. 

   more » « less
3. Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion

   https://doi.org/10.1007/978-3-030-25540-4_4  

   Bansal, Suguman (July 2019, Computer-Aided Verification)

   Discounted-sum inclusion (DS-inclusion, in short) formalizes the goal of comparing quantitative dimensions of systems such as cost, resource consumption, and the like, when the mode of aggregation for the quantitative dimension is discounted-sum aggregation. Discounted-sum comparator automata, or DS-comparators in short, are Buechi automata that read two in nite sequences of weights synchronously and relate their discounted-sum. Recent empirical investigations have shown that while DS-comparators enable competitive algorithms for DS-inclusion, they still suffer from the scalability bottleneck of Bueuchi operations. Motivated by the connections between discounted-sum and Buechi automata, this paper undertakes an investigation of language-theoretic properties of DS-comparators in order to mitigate the challenges of Buechi DS-comparators to achieve improved scalability of DS-inclusion. Our investigation uncovers that DS-comparators possess safety and co-safety language-theoretic properties. As a result, they enable reductions based on subset construction-based methods as opposed to higher complexity Buechi complementation, yielding tighter worst-case complexity and improved empirical scalability for DS-inclusion. 

   more » « less
4. Comparison of Staggered and In-Line V-Shaped Dimple Arrays Using S-PIV

   https://doi.org/10.1115/GT2015-43499  

   Brown, Charles P.; Wright, Lesley M.; McClain, Stephen T. (June 2015, ASME Turbo Expo 2015: Turbine Technical Conference and Exposition)

   As a result of the reduced pressure loss relative to ribs, recessed dimples have the potential to increase the thermal performance of internal cooling passages. In this experimental investigation, a Stereo-Particle Image Velocimetry (S-PIV) technique is used to characterize the three-dimensional, internal flow field over V-shaped dimple arrays. These flowfield measurements are combined with surface heat transfer measurements to fully characterize the performance of the proposed V-shaped dimples. This study compares the performance of two arrays. Both a staggered array and an in-line array of V-shaped dimples are considered. The layout of these V-shaped dimples is derived from a traditional, staggered hemispherical dimple array. The individual V-shaped dimples follow the same geometry, with depths of δ / D = 0.30. In the case of the in-line pattern, the spacing between the V-shaped dimples is 3.2D in both the streamwise and spanwise directions. For the staggered pattern, a spacing of 3.2D in the spanwise direction and 1.6D in the streamwise direction is examined. Each of these patterns was tested on one wide wall of a 3:1 rectangular channel. The Reynolds numbers examined range from 10000 to 37000. S-PIV results show that as the Reynolds numbers increase, the strength of the secondary flows induced by the in-line array increases, enhancing the heat transfer from the surface, without dramatically increasing the measured pressure drop. As a result of a minimal increase in pressure drop, the overall thermal performance of the channel increases as the Reynolds number increases (up to the maximum Reynolds number of 37000). 

   more » « less
5. Performance analysis of DNA crossbar arrays for high-density memory storage applications

   https://doi.org/10.1038/s41598-023-33004-6  

   De, Arpan; Mohammad, Hashem; Wang, Yiren; Kubendran, Rajkumar; Das, Arindam K.; Anantram, M. P. (April 2023, Scientific Reports)

   Abstract Deoxyribonucleic acid (DNA) has emerged as a promising building block for next-generation ultra-high density storage devices. Although DNA has high durability and extremely high density in nature, its potential as the basis of storage devices is currently hindered by limitations such as expensive and complex fabrication processes and time-consuming read–write operations. In this article, we propose the use of a DNA crossbar array architecture for an electrically readable read-only memory (DNA-ROM). While information can be ‘written’ error-free to a DNA-ROM array using appropriate sequence encodings its read accuracy can be affected by several factors such as array size, interconnect resistance, and Fermi energy deviations from HOMO levels of DNA strands employed in the crossbar. We study the impact of array size and interconnect resistance on the bit error rate of a DNA-ROM array through extensive Monte Carlo simulations. We have also analyzed the performance of our proposed DNA crossbar array for an image storage application, as a function of array size and interconnect resistance. While we expect that future advances in bioengineering and materials science will address some of the fabrication challenges associated with DNA crossbar arrays, we believe that the comprehensive body of results we present in this paper establishes the technical viability of DNA crossbar arrays as low power, high-density storage devices. Finally, our analysis of array performance vis-à-vis interconnect resistance should provide valuable insights into aspects of the fabrication process such as proper choice of interconnects necessary for ensuring high read accuracies. 

   more » « less