2 citations · 4 across the 5 of their papers we have counts for
11 papers
Reasoning About Vectors using an SMT Theory of Sequences
Ying Sheng, Andres Nötzli, Andrew Reynolds +7
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 progra…
lazybvtoint at the SMT Competition 2020
Yoni Zohar, Ahmed Irfan, Makai Mann +3
lazybvtoint is a new prototype SMT-solver, that will participate in the incremental and non-incremental tracks of the \qfbv logic.
Politeness and Stable Infiniteness: Stronger Together
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
We make two contributions to the study of polite combination in satisfiability modulo theories. The first contribution is a separation between politeness and strong politeness, by…
Politeness for the Theory of Algebraic Datatypes
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable versi…
Resources: A Safe Language Abstraction for Money
Sam Blackshear, David L. Dill, Shaz Qadeer +4
Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract pr…
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar +2
This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vect…