Zobrazeno 1 - 10
of 50
pro vyhledávání: '"Rinetzky, Noam"'
We address the problem of constraint encoding explosion which hinders the applicability of state merging in symbolic execution. Specifically, our goal is to reduce the number of disjunctions and if-then-else expressions introduced during state mergin
Externí odkaz:
http://arxiv.org/abs/2308.12068
Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of in ductive quantified loop invariants which, in some cases, may not even be firstorder expressible. In this paper, we suggest
Externí odkaz:
http://arxiv.org/abs/2106.00937
Autor:
Feldman, Yotam M. Y., Khyzha, Artem, Enea, Constantin, Morrison, Adam, Nanevski, Aleksandar, Rinetzky, Noam, Shoham, Sharon
Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously
Externí odkaz:
http://arxiv.org/abs/2010.00911
Data race free (DRF) programs constitute an important class of concurrent programs. In this paper we provide a framework for designing and proving the correctness of data flow analyses that target this class of programs. These analyses are in the sam
Externí odkaz:
http://arxiv.org/abs/2009.02775
Publikováno v:
Proceedings of the 2019 International Conference on Management of Data, SIGMOD Conference 2019, Amsterdam, The Netherlands, pages 537--554
Data analytics often involves hypothetical reasoning: repeatedly modifying the data and observing the induced effect on the computation result of a data-centric application. Previous work has shown that fine-grained data provenance can help make such
Externí odkaz:
http://arxiv.org/abs/2007.05400
Publikováno v:
2019 IEEE 35th International Conference on Data Engineering (ICDE), Macao, Macao, 2019, pp. 2016--2019
Data analytics often involves hypothetical reasoning: repeatedly modifying the data and observing the induced effect on the computation result of a data-centric application. Recent work has proposed to leverage ideas from data provenance tracking tow
Externí odkaz:
http://arxiv.org/abs/2007.05389
Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they exe
Externí odkaz:
http://arxiv.org/abs/1805.03992
Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often would like to access the same data both inside and outside transactions,
Externí odkaz:
http://arxiv.org/abs/1801.04249
Autor:
Grossman, Shelly, Abraham, Ittai, Golan-Gueta, Guy, Michalevsky, Yan, Rinetzky, Noam, Sagiv, Mooly, Zohar, Yoni
Callbacks are essential in many programming environments, but drastically complicate program understanding and reasoning because they allow to mutate object's local states by external objects in unexpected fashions, thus breaking modularity. The famo
Externí odkaz:
http://arxiv.org/abs/1801.04032
Autor:
Itzhaky, Shachar, Kotek, Tomer, Rinetzky, Noam, Sagiv, Mooly, Tamir, Orr, Veith, Helmut, Zuleger, Florian
A large number of web applications is based on a relational database together with a program, typically a script, that enables the user to interact with the database through embedded SQL queries and commands. In this paper, we introduce a method for
Externí odkaz:
http://arxiv.org/abs/1610.02101