EDBT 2026 Demo / reviewers in the wild / expert
Yoav Rodeh
dblp:50/2906
· DBLP profile ↗
26ranked-venue papers
2as first author
3since 2021 · last 2025
0000-0002-7224-6451ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 25 · 2 first-author · 3 since 2021Software engineering, systems software and programming languages · 5 · 1 first-authorArtificial intelligence and machine learning · 1 · 1 since 2021Applied, interdisciplinary, general and emerging computing · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | The Query Complexity of Searching Trees with Permanently Noisy AdviceabstractWe consider a search problem on trees aiming to find a treasure that an adversary places at one of the nodes. The algorithm can query nodes and extract directional information from them. That is, each node holds a pointer, termed advice , to one of its neighbors. Ideally, this advice points to the neighbor that is closer to the treasure, however, with probability \(q\) this advice points to a uniformly random neighbor. Crucially, the advice is permanent , hence querying the same node again yields the same answer. Let \(\Delta\) denote the maximal degree. Roughly speaking, we show that the expected number of queries incurs a phase transition when \(q\) is about \(1/\sqrt{\Delta}\) . In a recent paper, at TALG’21, we showed that if \(q\) is above the threshold then the expected number of queries is polynomial in \(n\) . Here, we prove that below the threshold, the expected number of queries is \(\mathcal{O}(\sqrt{\Delta}\log\Delta\cdot\log^{2}n)\) , which is tight up to an \(\mathcal{O}(\log n)\) factor when \(\Delta\) is small. We further show that this factor can be reduced to \(\mathcal{O}(\log\log n)\) in the case of regular trees and assuming that \(q for sufficiently small \(c>0\) . In addition, we study the case that the treasure must be found with some given probability. We show that for every fixed \(\varepsilon,\delta>0\) , if \(q<1/\Delta^{\varepsilon}\) then there exists a search strategy that with probability \(1-\delta\) finds the treasure using \((\delta^{-1}\log n)^{O(\frac{1}{\varepsilon})}\) queries, whereas \((\delta^{-1}\log n)^{\Omega(\frac{1}{\varepsilon})}\) queries are necessary. Lucas Boczkowski, Uriel Feige, Amos Korman, Yoav Rodeh |
ACM Trans. Algorithms | 4 |
| 2023 | Overapproximation of Non-Linear Integer Arithmetic for Smart Contract VerificationabstractThe need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover: overapproximation of non-linear integer arithmetic using linear integer arithmetic and using non-linear real arithmetic. We compare the performance of contemporary SMT solvers on verification conditions produced by the Certora Prover using these two approximations against the natural non-linear integer arithmetic encoding. Our evaluation shows that the use of the overapproximation methods leads to solving a significant number of new problems. Petra Hozzová, Jaroslav Bendík, Alexander Nutz, Yoav Rodeh |
LPAR | 4 |
| 2021 | Navigating in Trees with Permanently Noisy AdviceabstractWe consider a search problem on trees in which an agent starts at the root of a tree and aims to locate an adversarially placed treasure, by moving along the edges, while relying on local, partial information. Specifically, each node in the tree holds a pointer to one of its neighbors, termedadvice. A node is faulty with probabilityq. The advice at a non-faulty node points to the neighbor that is closer to the treasure, and the advice at a faulty node points to a uniformly random neighbor. Crucially, the advice ispermanent, in the sense that querying the same node again would yield the same answer. Let Δ denote the maximum degree. For the expected number of moves (edge traversals) until finding the treasure, we show that a phase transition occurs when thenoise parameterqis roughly 1 √Δ. Below the threshold, there exists an algorithm with expected number of movesO(D√Δ), whereDis the depth of the treasure, whereas above the threshold, every search algorithm has an expected number of moves, which is both exponential inDand polynomial in the number of nodes n. In contrast, if we require to find the treasure with probability at least 1 − δ, then for every fixed ɛ > 0, ifq< 1/Δɛ, then there exists a search strategy that with probability 1 − δ finds the treasure using (Δ−1D)O(1/ε)moves. Moreover, we show that (Δ−1D)Ω(1/ε)moves are necessary. Lucas Boczkowski, Uriel Feige, Amos Korman, Yoav Rodeh |
ACM Trans. Algorithms | 4 |
| 2020 | Multi-round cooperative search games with multiple players
Amos Korman, Yoav Rodeh |
J. Comput. Syst. Sci. | 2 |
| 2019 | Multi-Round Cooperative Search Games with Multiple Players
Amos Korman, Yoav Rodeh |
ICALP | 2 |
| 2019 | Parallel Bayesian Search with No CoordinationabstractCoordinating the actions of agents (e.g., volunteers analyzing radio signals in SETI@home) yields efficient search algorithms. However, such an efficiency is often at the cost of implementing complex coordination mechanisms which may be expensive in terms of communication and/or computation overheads. Instead, non-coordinating algorithms, in which each agent operates independently from the others, are typically very simple, and easy to implement. They are also inherently robust to slight misbehaviors, or even crashes of agents. In this article, we investigate the “price of non-coordinating,” in terms of search performance, and we show that this price is actually quite small. Specifically, we consider a parallel version of a classical Bayesian search problem, where set of k ≥1 searchers are looking for a treasure placed in one of the boxes indexed by positive integers, according to some distribution p . Each searcher can open a random box at each step, and the objective is to find the treasure in a minimum number of steps. We show that there is a very simple non-coordinating algorithm which has expected running time at most 4(1−1/ k +1) 2 OPT+10, where OPT is the expected running time of the best fully coordinated algorithm. Our algorithm does not even use the precise description of the distribution p , but only the relative likelihood of the boxes. We prove that, under this restriction, our algorithm has the best possible competitive ratio with respect to OPT. For the case where a complete description of the distribution p is given to the search algorithm, we describe an optimal non-coordinating algorithm for Bayesian search. This latter algorithm can be twice as fast as our former algorithm in practical scenarios such as uniform distributions. All these results provide a complete characterization of non-coordinating Bayesian search. The take-away message is that, for their simplicity and robustness, non-coordinating algorithms are viable alternatives to complex coordinating mechanisms subject to significant overheads. Most of these results apply as well to linear search, in which the indices of the boxes reflect their relative importance, and where important boxes must be visited first. Pierre Fraigniaud, Amos Korman, Yoav Rodeh |
J. ACM | 3 |
| 2018 | Searching a Tree with Permanently Noisy AdviceabstractWe consider a problem of searching for an unknown target vertex t in a (possibly edge-weighted) graph. Each vertex-query points to a vertex v and the response either admits that v is the target or provides any neighbor s of v that lies on a shortest path from v to t. This model has been introduced for trees by Onak and Parys [FOCS 2006] and for general graphs by Emamjomeh-Zadeh et al. [STOC 2016]. In the latter, the authors provide algorithms for the error-less case and for the independent noise model (where each query independently receives an erroneous answer with known probability p<1/2 and a correct one with probability 1-p). We study this problem both with adversarial errors and independent noise models. First, we show an algorithm that needs at most (log_2 n)/(1 - H(r)) queries in case of adversarial errors, where the adversary is bounded with its rate of errors by a known constant r<1/2. Our algorithm is in fact a simplification of previous work, and our refinement lies in invoking an amortization argument. We then show that our algorithm coupled with a Chernoff bound argument leads to a simpler algorithm for the independent noise model and has a query complexity that is both simpler and asymptotically better than the one of Emamjomeh-Zadeh et al. [STOC 2016]. Our approach has a wide range of applications. First, it improves and simplifies the Robust Interactive Learning framework proposed by Emamjomeh-Zadeh and Kempe [NIPS 2017]. Secondly, performing analogous analysis for edge-queries (where a query to an edge e returns its endpoint that is closer to the target) we actually recover (as a special case) a noisy binary search algorithm that is asymptotically optimal, matching the complexity of Feige et al. [SIAM J. Comput. 1994]. Thirdly, we improve and simplify upon an algorithm for searching of unbounded domains due to Aslam and Dhagat [STOC 1991]. Lucas Boczkowski, Amos Korman, Yoav Rodeh |
ESA | 3 |
| 2018 | The Dependent Doors Problem: An Investigation into Sequential Decisions without FeedbackabstractWe introduce the dependent doors problem as an abstraction for situations in which one must perform a sequence of dependent decisions, without receiving feedback information on the effectiveness of previously made actions. Informally, the problem considers a set of d doors that are initially closed, and the aim is to open all of them as fast as possible. To open a door, the algorithm knocks on it, and it might open or not according to some probability distribution. This distribution may depend on which other doors are currently open, as well as on which other doors were open during each of the previous knocks on that door. The algorithm aims to minimize the expected time until all doors open. Crucially, it must act at any time without knowing whether or which other doors have already opened. In this work, we focus on scenarios where dependencies between doors are both positively correlated and acyclic. The fundamental distribution of a door describes the probability it opens in the best of conditions (with respect to other doors being open or closed). We show that if in two configurations of d doors corresponding doors share the same fundamental distribution, then these configurations have the same optimal running time up to a universal constant, no matter what the dependencies between doors and what the distributions. We also identify algorithms that are optimal up to a universal constant factor. For the case in which all doors share the same fundamental distribution, we additionally provide a simpler algorithm and a formula to calculate its running time. We furthermore analyse the price of lacking feedback for several configurations governed by standard fundamental distributions. In particular, we show that the price is logarithmic in d for memoryless doors but can potentially grow to be linear in d for other distributions. We then turn our attention to investigate precise bounds. Even for the case of two doors, identifying the optimal sequence is an intriguing combinatorial question. Here, we study the case of two cascading memoryless doors. That is, the first door opens on each knock independently with probability p 1 . The second door can only open if the first door is open, in which case it will open on each knock independently with probability p 2 . We solve this problem almost completely by identifying algorithms that are optimal up to an additive term of 1. Amos Korman, Yoav Rodeh |
ACM Trans. Algorithms | 2 |
| 2017 | The Dependent Doors Problem: An Investigation into Sequential Decisions without Feedback
Amos Korman, Yoav Rodeh |
ICALP | 2 |
| 2017 | Parallel Search with No Coordination
Amos Korman, Yoav Rodeh |
SIROCCO | 2 |
| 2017 | Fast rendezvous on a cycle by agents with different speeds
Ofer Feinerman, Amos Korman, Shay Kutten, Yoav Rodeh |
Theor. Comput. Sci. | 4 |
| 2016 | Parallel exhaustive search without coordinationabstractWe analyse parallel algorithms in the context of exhaustive search over totally ordered sets. Imagine an infinite list of “boxes”, with a “treasure” hidden in one of them, where the boxes’ order reflects the importance of finding the treasure in a given box. At each time step, a search protocol executed by a searcher has the ability to peek into one box, and see whether the treasure is present or not. Clearly, the best strategy of a single searcher would be to open the boxes one by one, in increasing order. Moreover, by equally dividing the workload between them, k searchers can trivially find the treasure k times faster than one searcher. However, this straightforward strategy is very sensitive to failures (e.g., crashes of processors), and overcoming this issue seems to require a large amount of communication. We therefore address the question of designing parallel search algorithms maximizing their speed-up and maintaining high levels of robustness, while minimizing the amount of resources for coordination. Based on the observation that algorithms that avoid communication are inherently robust, we focus our attention on identifying the best running time performance of non-coordinating algorithms. Specifically, we devise non-coordinating algorithms that achieve a speed-up of 9/8 for two searchers, a speed-up of 4/3 for three searchers, and in general, a speed-up of k/4(1+1/k)2 for any k≥ 1 searchers. Thus, asymptotically, the speed-up is only four times worse compared to the case of full coordination. Moreover, these bounds are tight in a strong sense as no non-coordinating search algorithm can achieve better speed-ups. Our algorithms are surprisingly simple and hence applicable. However they are memory intensive and so we suggest a practical, memory efficient version, with a speed-up of (k2 − 1)/4k. That is, it is only a factor of (k+1)/(k−1) slower than the optimal algorithm. Overall, we highlight that, in faulty contexts in which coordination between the searchers is technically difficult to implement, intrusive with respect to privacy, and/or costly in term of resources, it might well be worth giving up on coordination, and simply run our non-coordinating exhaustive search algorithms. Pierre Fraigniaud, Amos Korman, Yoav Rodeh |
STOC | 3 |
| 2010 | Constructing Labeling Schemes through Universal Matrices
Amos Korman, David Peleg, Yoav Rodeh |
Algorithmica | 3 |
| 2006 | Constructing Labeling Schemes Through Universal Matrices
Amos Korman, David Peleg, Yoav Rodeh |
ISAAC | 3 |
| 2006 | Building small equality graphs for deciding equality logic with uninterpreted functions
Yoav Rodeh, Ofer Strichman |
Inf. Comput. | 1 |
| 2004 | Labeling Schemes for Dynamic Tree Networks
Amos Korman, David Peleg, Yoav Rodeh |
Theory Comput. Syst. | 3 |
| 2003 | Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293)
Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
Inf. Comput. | 2 |
| 2002 | Labeling Schemes for Dynamic Tree Networks
Amos Korman, David Peleg, Yoav Rodeh |
STACS | 3 |
| 2002 | The Small Model Property: How Small Can It Be?
Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
Inf. Comput. | 2 |
| 2001 | The Temporal Logic Sugar
Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh |
CAV | 6 |
| 2001 | Finite Instantiations in Equivalence Logic with Uninterpreted Functions
Yoav Rodeh, Ofer Strichman |
CAV | 1 |
| 2001 | Range Allocation for Equivalence Logic
Amir Pnueli, Yoav Rodeh, Ofer Strichman |
FSTTCS | 2 |
| 2001 | Efficient Detection of Vacuity in Temporal Model Checking
Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh |
Formal Methods Syst. Des. | 4 |
| 1999 | Deciding Equality Formulas by Small Domains Instantiations
Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
CAV | 2 |
| 1997 | RuleBase: Model Checking at IBM
Ilan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, P. Paanah, Yoav Rodeh, G. Ronin, Yaron Wolfsthal |
CAV | 9 |
| 1997 | Efficient Detection of Vacuity in ACTL Formulaas
Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh |
CAV | 4 |