David Harel

ICML Conference 2025 Conference Paper

Accelerating LLM Inference with Lossless Speculative Decoding Algorithms for Heterogeneous Vocabularies

• Nadav Timor
• Jonathan Mamou
• Daniel Korat
• Moshe Berchansky
• Gaurav Jain
• Oren Pereg
• Moshe Wasserblat
• David Harel

Accelerating the inference of large language models (LLMs) is a critical challenge in generative AI. Speculative decoding (SD) methods offer substantial efficiency gains by generating multiple tokens using a single target forward pass. However, existing SD approaches require the drafter and target models to share the same vocabulary, thus limiting the pool of possible drafters, often necessitating the training of a drafter from scratch. We present three new SD methods that remove this shared-vocabulary constraint. All three methods preserve the target distribution (i. e. , they are lossless) and work with off-the-shelf models without requiring additional training or modifications. Empirically, on summarization, programming, and long-context tasks, our algorithms demonstrate significant speedups of up to 2. 8x over standard autoregressive decoding. By enabling any off-the-shelf model to serve as a drafter and requiring no retraining, this work substantially broadens the applicability of the SD framework in practice.

ICLR Conference 2025 Conference Paper

Distributed Speculative Inference (DSI): Speculation Parallelism for Provably Faster Lossless Language Model Inference

• Nadav Timor
• Jonathan Mamou
• Daniel Korat
• Moshe Berchansky
• Oren Pereg
• Moshe Wasserblat
• Tomer Galanti
• Michal Gordon-Kiwkowitz

This paper introduces *distributed speculative inference (DSI)*, a novel inference algorithm that is provably faster than speculative inference (SI) [leviathan2023, chen2023, miao2024, sun2025, timor2025] and standard autoregressive inference (non-SI). Like other SI algorithms, DSI operates on frozen language models (LMs), requiring no training or architectural modifications, and it preserves the target distribution. Prior studies on SI have demonstrated empirical speedups over non-SI—but rely on sufficiently fast and accurate drafters, which are often unavailable in practice. We identify a gap where SI can be slower than non-SI if drafters are too slow or inaccurate. We close this gap by proving that DSI is faster than both SI and non-SI—given any drafters. DSI is therefore not only faster than SI, but also unlocks the acceleration of LMs for which SI fails. DSI leverages *speculation parallelism (SP)*, a novel type of task parallelism, to orchestrate target and drafter instances that overlap in time, establishing a new foundational tradeoff between computational resources and latency. Our simulations show that DSI is 1.29-1.92x faster than SI in single-node setups for various off-the-shelf LMs and tasks. We open-source all our code.

AAAI Conference 2019 Conference Paper

Labor Division with Movable Walls: Composing Executable Specifications with Machine Learning and Search (Blue Sky Idea)

• David Harel
• Assaf Marron
• Ariel Rosenfeld
• Moshe Vardi
• Gera Weiss

Artificial intelligence (AI) techniques, including, e. g. , machine learning, multi-agent collaboration, planning, and heuristic search, are emerging as ever-stronger tools for solving hard problems in real-world applications. Executable specification techniques (ES), including, e. g. , Statecharts and scenario-based programming, is a promising development approach, offering intuitiveness, ease of enhancement, compositionality, and amenability to formal analysis. We propose an approach for integrating AI and ES techniques in developing complex intelligent systems, which can greatly simplify agile/spiral development and maintenance processes. The approach calls for automated detection of whether certain goals and sub-goals are met; a clear division between sub-goals solved with AI and those solved with ES; compositional and incremental addition of AI-based or ES-based components, each focusing on a particular gap between a current capability and a well-stated goal; and, iterative refinement of sub-goals solved with AI into smaller sub-sub-goals where some are solved with ES, and some with AI. We describe the principles of the approach and its advantages, as well as key challenges and suggestions for how to tackle them.

LPAR Conference 2013 Conference Paper

Relaxing Synchronization Constraints in Behavioral Programs

• David Harel
• Amir Kantor
• Guy Katz

Abstract In behavioral programming, a program consists of separate modules called behavior threads, each representing a part of the system’s allowed, necessary or forbidden behavior. An execution of the program is a series of synchronizations between these threads, where at each synchronization point an event is selected to be carried out. As a result, the execution speed is dictated by the slowest thread. We propose an eager execution mechanism for such programs, which builds upon the realization that it is often possible to predict the outcome of a synchronization point even without waiting for slower threads to synchronize. This allows faster threads to continue running uninterrupted, whereas slower ones catch up at a later time. Consequently, eager execution brings about increased system performance, better support for the modular design of programs, and the ability to distribute programs across several machines. It also allows to apply behavioral programming to a variety of problems that were previously outside its scope. We illustrate the method by concrete examples, implemented in a behavioral programming framework in C + +.

TCS Journal 2012 Journal Article

Multi-modal scenarios revisited: A net-based representation

• David Harel
• Amir Kantor

Live sequence charts (LSC) is a visual formalism that can be used to model reactive systems. In terms of LSC, a system model is a set of charts, each of which may be referred to as a multi-modal scenario. In this paper, we revisit the scenarios of the UML2-compliant dialect of LSC. We abstract from their concrete visual representation, and show how to capture multi-modal scenarios in a flexible, yet conservative, way. For this, we use the building blocks of Petri nets; i. e. , places and transitions, extended with modalities and interpreted in accordance with the semantics of LSC. This results in what we refer to as LSC nets. LSC nets can express a variety of advanced constructs of LSC, as well as several semantic variations suggested in the literature, with just a few primitive notions. At the same time, the net corresponding to an LSC involves rather superficial, technical, changes in presentation. As a result, LSC nets form a rigorous basis to present, discuss, and investigate the language as a whole, or interesting fragments thereof.

TCS Journal 2008 Journal Article

GemCell: A generic platform for modeling multi-cellular biological systems

• Hila Amir-Kroll
• Avital Sadot
• Irun R. Cohen
• David Harel

The mass and complexity of biological information requires computer-aided simulation and analysis to help scientists achieve understanding and guide experimentation. Although living organisms are composed of cells, actual genomic and proteomic data have not yet led to a satisfactory model of working cell in silico. We have set out to devise a user-friendly generic platform, GemCell, for Generic Executable Modeling of Cells, based on whole, functioning cells. Starting with the cell simplifies life, because all cells expresses essentially five generic types of behavior: replication, death, movement (including change of shape and adherence), export (secretion, signaling, etc.) and import (receiving signals, metabolites, phagocytosis, etc.). The details of these behaviors are specified in GemCell for particular kinds of cells as part of a database of biological specifics (the DBS), which specifies the cell properties and functions that depend on the cell’s history, state, environment, etc. The DBS is designed in an intuitive fashion, so users are able to easily insert their data of interest. The generic part of GemCell, built using Statecharts, is a fully dynamic model of a cell, its interactions with the environment and its resulting behavior, individually and collectively. Model specificity emerges from the DBS, so that model execution is carried out by the statecharts executing with the aid of specific data extracted from the DBS dynamically. Our long term goal is for GemCell to serve as a broadly applicable platform for biological modeling and analysis, supporting user-friendly in silico experimentation, animation, discovery of emergent properties, and hypothesis testing, for a wide variety of biological systems.

I&C Journal 2002 Journal Article

On the Complexity of Verifying Concurrent Transition Systems

• David Harel
• Orna Kupferman
• Moshe Y. Vardi

In implementation verification, we check that an implementation is correct with respect to a specification by checking whether the behaviors of a transition system that models the program's implementation correlate with the behaviors of a transition system that models its specification. In this paper, we investigate the effect of concurrency on the complexity of implementation verification. We consider trace-based and tree-based approaches to the verification of concurrent transition systems, with and without fairness. Our results show that in almost all cases the complexity of the problem is exponentially harder than that of the sequential case. Thus, as in the model-checking verification methodology, the state-explosion problem cannot be avoided.

MFCS Conference 1998 Invited Paper

Towards a Theory of Recursive Structures

• David Harel

Abstract In computer science, one is interested mainly in finite objects. Insofar as infinite objects are of interest, they must be computable, i. e. , recursive, thus admitting an effective finite representation. This leads to the notion of a recursive graph, or, more generally, a recursive structure, model or data base. This paper summarizes recent work on recursive structures and data bases, including (i) the high undecidability of many problems on recursive graphs and structures, (ii) a method for deducing results on the descriptive complexity of finitary NP optimization problems from results on the computational complexity (i. e. , the degree of undecidability) of their infinitary analogues, (iii) completeness results for query languages on recursive data bases, (iv) correspondences between descriptive and computational complexity over recursive structures, and (v) zero-one laws for recursive structures.

TCS Journal 1996 Journal Article

Complexity results for two-way and multi-pebble automata and their logics

• Noa Globerman
• David Harel

Two-way and multi-pebble automata are considered (the latter appropriately restricted to accept only regular languages), and enriched with additional features, such as nondeterminism and concurrency. We investigate the succinctness of such machines, and the extent to which this succinctness carries over to make the reasoning problem in propositional dynamic logic more difficult. The two main results establish that each additional pebble provides inherent exponential power on both fronts.

I&C Journal 1996 Journal Article

More on Nonregular PDL: Finite Models and Fibonacci-like Programs

• David Harel
• Eli Singerman

We continue research on enriching propositional dynamic logic (PDL) with nonregular programs. Previous work indicates that the general problem of characterizing those extensions for which PDL becomes undecidable is probably very hard. After observing that any nonregular extension increases the expressive power of PDL, we concentrate on one-letter extensions. First, we address the issue of finite models: A general condition is formulated, and is proven to be sufficient for a one-letter extension to violate the finite model property. We show the condition to hold in several cases, including all polynomials, sums of primes, and linear recurrences. We then build on a technique of Paterson and Harel, and show that the validity problem for PDL enriched with any Fibonacci-like sequence isΠ 1 1-complete.

TCS Journal 1994 Journal Article

On the solvability of domino snake problems

• Yael Etzion-Petruschka
• David Harel
• Dale Myers

In this paper we present an extensive treatment of tile connectability problems, sometimes called domino snake problems. The interest in such problems stems from their relationship to classical tiling problems, which have been established as an important, simple and useful tool for obtaining basic lower bound results in complexity and computability theory. We concentrate on the following two contrasting results: The general snake problem is undecidable in a half-plane (due to Ebbinghaus), but is decidable in the whole plane. This surprising decidability result was announced without proof by Myers in 1979. We provide here the first full proof, and show that the problem is actually PSPACE-complete. We also prove many results concerning the difficulty of variants of these general snake problems and their extension to infinite snakes. In addition, we establish a resemblance between snake problems and classical tiling problems, considering the corresponding bounded, unbounded and recurring cases.

STOC Conference 1991 Conference Paper

Hamiltonian Paths in Infinite Graphs

• David Harel

FOCS Conference 1990 Conference Paper

Deciding Properties of Nonregular Programs (Preliminary Version)

• David Harel
• Danny Raz

The problem of deciding the validity of formulas in extensions of propositional dynamic logic (PDL) is considered. The extensions are obtained by adding programs defined by nonregular languages. In the past, a number of very simple languages were shown to render this problem highly undecidable, whereas other very similar-looking languages were shown to retain decidability. Understanding this rather strange phenomenon and generalizing the isolated extensions have remained elusive. The authors provide decision procedures for two wide classes of extensions, thus shedding light on the general problem. The proofs are novel, in that they explicitly consider the machines that accept the languages, in this case special classes of PDAs and stack automata. It is shown that the emptiness problem for stack automata on infinite trees is decidable, a result of independent interest, and the result is combined with the construction of certain tree models for the corresponding formulas. >

MFCS Conference 1989 Invited Paper

A Thesis for Bounded Concurrency

• David Harel

Abstract In recent work, we have investigated the power of bounded cooperative concurrency. The underlying notion involves enriching computational devices with a bounded number of concurrent components that communicate, synchronize, or otherwise cooperate. Comparisons involving succinctness and the time complexity of reasoning about programs have been undertaken. The results, which are extremely robust, show that in all the cases we have addressed bounded cooperative concurrency is of inherent exponential power, regardless of whether nondeterminism and/or pure, unbounded parallelism are also present. In this expository paper we motivate the research and survey the main results.

STOC Conference 1984 Conference Paper

A General Result on Infinite Trees and Its Applications (Preliminary Report)

• David Harel

STOC Conference 1982 Conference Paper

A Probabilistic Dynamic Logic

• Yishai A. Feldman
• David Harel

TCS Journal 1981 Journal Article

On the total correctness of nondeterministic programs

• David Harel

For an arbitrary programming language with nondeterminism to be implementable, the existence of computation trees modelling the possible changes in state in the course of a computation is postulated. A general definition of what constitutes an execution method is then presented. Falling naturally out of these ideas is the correspondence between execution methods and total correctness, in that different properties are required of a program to be correct when different methods are adopted. We describe a variety of plausible methods of execution falling under the general definition and single out four particular ones. The arguments made are then illustrated by analysing the properties required by Dijkstra of guarded commands in view of these four methods. We conclude that a general approach such as that suggested here seems to be needed for dealing with programming languages and execution methods other than the particular ones treated by Dijkstra.

FOCS Conference 1981 Conference Paper

Propositional Dynamic Logic of Context-Free Programs

• David Harel
• Amir Pnueli
• Jonathan Stavi

The borderline between decidable and undecidable Propositional Dynamic Logic (PDL) is sought when iterative programs represented by regular expressions are augmented with increasingly more complex recursive programs represented by context-free languages. The results in this paper and its companion [HPS] indicate that this line is extremely close to the original regular PDL. The main result of the present paper is: The validity problem for PDL with additional programs αΔ(β)γΔ for regular α, β and γ, defined as Uiαi; β; γi, is Π11-complete. One of the results of [HPS] shows that the single program AΔ(B) AΔ for atomic A and B is actually sufficient for obtaining Π11- completeness. However, the proofs of this paper use different techniques which seem to be worthwhile in their own right.

MFCS Conference 1980 Conference Paper

on And/Or Schemes

• David Harel

Abstract A computational model, based on and/or subgoaling, is described. It is shown that various models of computation, such as recursive program schemes, decision trees and combinational networks, are naturally embedded in the and/or language. These observations pose some interesting questions for further research. As a first result in the metatheory of and/or schemes, we prove a normal form theorem showing that with the addition of “auxiliary variables”, every and/or scheme is strongly equivalent to one with “and/or depth” equal to 1.

FOCS Conference 1980 Conference Paper

Process Logic: Expressiveness, Decidability, Completeness

• David Harel
• Dexter Kozen
• Rohit Parikh

We define a process logic PL that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL is an extension of the language of Propositional Dynamic Logic (PDL). We give a deductive system for PL which includes the Segerberg axioms for PDL and prove that it is complete. We also show that PL is decidable.

TCS Journal 1980 Journal Article

Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic

• David Harel

The simple set WL of deterministic while programs is defined and a number of known methods for proving the correctness of these programs are surveyed. Emphasis is placed on the tradeoff existing between data-directed and syntax-directed methods, and on providing, especially for the latter, a uniform description enabling comparison and assessment. Among the works considered are the Floyd/Hoare invariant assertion method for partial correctness, Floyd's well-founded sets method for termination, Dijkstra's notion of weakest precondition, the Burstall/Manna and Waldinger intermittent assertion method and more. Also, a brief comparison is carried out between three logics of programs: dynamic logic, algorithmic logic and programming logic.

FOCS Conference 1980 Conference Paper

Structure and Complexity of Relational Queries

• Ashok K. Chandra
• David Harel

This paper is an attempt at laying the foundations for the classification of queries on relational data bases according to their structure and their computational complexity. Using the operations of composition and fixpoints, a Σ-Π hierarchy of height, ω2, called the fixpoint query hierarchy, is defined, and its properties investigated. The hierarchy includes most of the queries considered in the literature including those of Codd and Aho and Ullman. The hierarchy to level ω characterizes the first-order queries, and the levels up to ω are shown to be strict. Sets of queries larger than the fixpoint query hierarchy are obtained by considering the queries computable in polynomial time, queries computable in polynomial space, etc. It is shown that classes of queries defined from such complexity classes behave (with respect to containment) in a manner very similar to the corresponding complexity classes. Also, the set of second-order queries turns out to be the same as the set of queries defined from the polynomialtime hierarchy. Finally, these classes of queries are used to characterize a set of queries defined from language considerations: those expressible in a programming language with only typed (or ranked) relation variables. At the end of the paper is a list of symbols used therein.

STOC Conference 1979 Conference Paper

Computable Queries for Relational Data Bases (Preliminary Report)

• Ashok K. Chandra
• David Harel

STOC Conference 1977 Conference Paper

A Complete Axiomatic System for Proving Deductions about Recursive Programs

• David Harel
• Amir Pnueli
• Jonathan Stavi

STOC Conference 1977 Conference Paper

Computability and Completeness in Logics of Programs (Preliminary Report)

• David Harel
• Albert R. Meyer
• Vaughan R. Pratt