Colloquia and Seminars

Constrained Horn Clauses (CHCs) have emerged as a powerful framework for formal verification, enabling reasoning about program safety, invariant synthesis, model checking, and related verification tasks. Their combination of logical expressiveness and algorithmic solvability has made CHCs a central foundation for modern verification techniques. However, despite significant advances in CHC solving, reasoning about low-level bit-precise program semantics remains a major challenge for existing solvers.

Traditionally, a set of CHCs is encoded with respect to a single background theory. In the context of bit-precise verification, program semantics can naturally be encoded as CHCs modulo the theory of fixed-size bit-vectors. Alternatively, bit-precise semantics can be encoded using integer arithmetic by modeling modular and bit-wise behavior through arithmetic constraints. However, neither approach consistently yields an efficient verification procedure: reasoning directly in the bit-vector theory often limits the scalability and generalization capabilities of CHC solvers, whereas arithmetic encodings produce complex constraints that are expensive to process, especially in the presence of bit-wise operations.

To address this limitation, I will present a novel theory-modular framework for CHC satisfiability that enables coordinated reasoning across multiple background theories. The framework decomposes a CHC system into complementary fragments interpreted over different background theories and coordinates reasoning between them through sound cross-theory transformations. This modular approach combines efficient arithmetic reasoning with precise handling of bit-level operations, leveraging the strengths of both theories within a unified CHC-solving framework.

I will describe the theoretical foundations of the approach, including theory transformations, modular CHC encodings, and a satisfiability procedure for coordinated reasoning across theories. I will also present experimental results on bit-manipulating verification benchmarks, demonstrating substantial improvements over monolithic single-theory approaches. Finally, I will discuss how theory-modular reasoning can contribute to future directions in scalable and expressive CHC solving.

High-performance computing software must be ported among serial C++, OpenMP, and CUDA as platforms and deployment constraints change. Such translation requires preserving program behavior while satisfying target-specific constraints on parallel execution, synchronization, memory movement, and API use. Although large language models are flexible code generators, plausible parallel-code translations can fail at compilation, execution, or validation.

We study guidance and adaptation methods that make existing LLMs more reliable without training a generator from scratch. The central method is latent PRM guidance, which guides a frozen latent-reasoning model before code is emitted. A small process reward model scores alternative continuous hidden-state branches during latent reasoning and selects branches expected to lead to executable, behaviorally correct programs. The evaluation also includes lighter-weight assistance methods such as prompting, fine-tuning, and iterative repair with compiler and execution feedback.

On the ParaTrans dataset, LLMs struggle as standalone executable translators, but their reliability improves significantly through task-aware assistance. Latent PRM guidance improves validation over unguided latent reasoning while remaining compatible with iterative repair. The best results are achieved through the cumulative and compounding effects of combining guidance, prompting, and iterative repair to improve executable correctness and validation performance.

Modern text-to-image models achieve strong visual fidelity and prompt alignment, but often at the cost of generative diversity. In this talk, I will present two complementary approaches to this problem: a simple inference-time method that achieves rich diversity by intervening in the model’s internal representations, and a new task formulation of controlled diversity, where users explore structured image galleries through meaningful semantic variations.

Omer Dahary is a PhD student in Computer Science at Tel Aviv University, advised by Daniel Cohen-Or. His research focuses on generative models, with an emphasis on improving their ability to align with user control. He received dual B.Sc. degrees in Computer Science and Mathematics from the Technion through the Rothschild Excellence Program, and subsequently earned his M.Sc. at the Technion under the supervision of Alex Bronstein.

Prediction algorithms are increasingly used to inform decisions about humans, but maximizing accuracy - the standard learning objective - does not necessarily maximize user benefits. Instead, we propose optimizing social welfare, defined as the average gain users receive from correct predictions. Welfare enables to express, and therefore account for, heterogeneity in how much users benefit from accuracy. But since these valuations are private and users can gain from overreporting them, learning must simultaneously elicit truthful values and optimize welfare with respect to them. To this end, we propose a novel learning algorithm that incorporates a truthful auction. We show how to compute allocations and prices efficiently, and bound the number of paying users - which surprisingly is independent of the sample size. We conclude with experiments on real and synthetic data that demonstrate our algorithm and explore the connections between welfare and accuracy.

We initiate the study of  DNA-based distributed storage systems, where information is encoded across multiple DNA data storage containers to achieve robustness against container failures. In this setting, data are distributed over M containers, and the objective is to guarantee that the contents of any failed container can be reliably reconstructed from the surviving ones. Unlike classical distributed storage systems, DNA data storage containers are fundamentally constrained by sequencing technology, since each read operation yields the content of  a uniformly random sampled strand from the container. Within this framework, we consider several erasure-correcting codes and analyze the expected recovery time of the data stored in a failed container. Our results are obtained by analyzing generalized versions of the classical Coupon Collector's Problem, which may be of independent interest.

Selected for an oral presentation at CVPR 2026; Image classification is a well-studied task in computer vision, and yet it remains challenging under high-uncertainty conditions, such as when input images are corrupted or training data are limited. Conventional classification approaches typically train models to directly predict class labels from input images, but this might lead to suboptimal performance in such scenarios. To address this issue, we propose Discrete Diffusion Classification Modeling (DiDiCM), a novel framework that leverages a diffusion-based procedure to model the posterior distribution of class labels conditioned on the input image. DiDiCM supports diffusion-based predictions either on class probabilities or on discrete class labels, providing flexibility in computation and memory trade-offs. We conduct a comprehensive empirical study demonstrating the superior performance of DiDiCM over standard classifiers, showing that a few diffusion iterations achieve higher classification accuracy on the ImageNet dataset compared to baselines, with accuracy gains increasing as the task becomes more challenging.