arXiv subjects

Gal Amram

Publications and source records attributed to Gal Amram.

13 recordsLinked to original sources

arXiv2025

Vintage Code, Modern Judges: Meta-Validation in Low Data Regimes

Application modernization in legacy languages such as COBOL, PL/I, and REXX faces an acute shortage of resources, both in expert availability and in high-quality human evaluation data. While Large Language Models as a Judge (LaaJ) offer a scalable alternative to expert review, their reliability must be validated before being trusted in high-stakes workflows. Without principled validation, organizations risk a circular evaluation loop, where unverified LaaJs are used to assess model outputs, potentially reinforcing unreliable judgments and compromising downstream deployment decisions. Although various automated approaches to validating LaaJs have been proposed, alignment with human judgment remains a widely used and conceptually grounded validation strategy. In many real-world domains, the availability of human-labeled evaluation data is severely limited, making it difficult to assess how well a LaaJ aligns with human judgment. We introduce SparseAlign, a formal framework for assessing LaaJ alignment with sparse human-labeled data. SparseAlign combines a novel pairwise-confidence concept with a score-sensitive alignment metric that jointly capture ranking consistency and score proximity, enabling reliable evaluator selection even when traditional statistical methods are ineffective due to limited annotated examples. SparseAlign was applied internally to select LaaJs for COBOL code explanation. The top-aligned evaluators were integrated into assessment workflows, guiding model release decisions. We present a case study of four LaaJs to demonstrate SparseAlign's utility in real-world evaluation scenarios.

cs.SE↗

arXiv2025

LaajMeter: A Framework for LaaJ Evaluation

Large Language Models (LLMs) are increasingly used as evaluators in natural language processing tasks, a paradigm known as LLM-as-a-Judge (LaaJ). The analysis of a LaaJ software, commonly refereed to as meta-evaluation, pose significant challenges in domain-specific contexts. In such domains, in contrast to general domains, annotated data is scarce and expert evaluation is costly. As a result, meta-evaluation is often performed using metrics that have not been validated for the specific domain in which they are applied. Therefore, it becomes difficult to determine which metrics effectively identify LaaJ quality, and further, what threshold indicates sufficient evaluator performance. In this work, we introduce LaaJMeter, a simulation-based framework for controlled meta-evaluation of LaaJs. LaaJMeter enables engineers to generate synthetic data representing virtual models and judges, allowing systematic analysis of evaluation metrics under realistic conditions. This helps practitioners validate LaaJs for specific tasks: they can test whether their metrics correctly distinguish between high and low quality (virtual) LaaJs, and estimate appropriate thresholds for evaluator adequacy. We demonstrate the utility of LaaJMeter in a code translation task involving a legacy programming language, showing how different metrics vary in sensitivity to evaluator quality. Our results highlight the limitations of common metrics and the importance of principled metric selection. LaaJMeter provides a scalable and extensible solution for assessing LaaJs in low-resource settings, contributing to the broader effort to ensure trustworthy and reproducible evaluation in NLP.

cs.CL↗

arXiv2025

Black-Box Bug-Amplification for Multithreaded Software

Bugs, especially those in concurrent systems, are often hard to reproduce because they manifest only under rare conditions. Testers frequently encounter failures that occur only under specific inputs, even when occurring with low probability. We propose an approach to systematically amplify the occurrence of such elusive bugs. We treat the system under test as a black-box and use repeated trial executions to train a predictive model that estimates the probability of a given input configuration triggering a bug. We evaluate this approach on a dataset of 17 representative concurrency bugs spanning diverse categories. Several model-based search techniques are compared against a brute-force random sampling baseline. Our results show that an ensemble of regression models can significantly increase bug occurrence rates across nearly all scenarios, often achieving an order-of-magnitude improvement over random sampling. The contributions of this work include: (i) a novel formulation of bug-amplification as a rare-event regression problem; (ii) an empirical evaluation of multiple techniques for amplifying bug occurrence, demonstrating the effectiveness of model-guided search; and (iii) a practical, non-invasive testing framework that helps practitioners expose hidden concurrency faults without altering the internal system architecture.

cs.SE↗

arXiv2025

Automata Models for Effective Bug Pattern Description

Debugging complex systems is a crucial yet time-consuming task. This paper presents the use of automata learning and testing techniques to obtain concise and informative bug descriptions. We introduce the concepts of Failure Explanations (FE), Eventual Failure Explanations (EFE), and Early Detection (ED) to provide meaningful summaries of failing behavior patterns. By factoring out irrelevant information and focusing on essential test patterns, our approach aims to enhance bug detection and understanding. We evaluate our methods using various test patterns and real-world benchmarks, demonstrating their effectiveness in producing compact and informative bug descriptions.

cs.SE↗

arXiv2021

Adapting Behaviors via Reactive Synthesis

In the \emph{Adapter Design Pattern}, a programmer implements a \emph{Target} interface by constructing an \emph{Adapter} that accesses an existing \emph{Adaptee} code. In this work, we present a reactive synthesis interpretation to the adapter design pattern, wherein an algorithm takes an \emph{Adaptee} and a \emph{Target} transducers, and the aim is to synthesize an \emph{Adapter} transducer that, when composed with the {\em Adaptee}, generates a behavior that is equivalent to the behavior of the {\em Target}. One use of such an algorithm is to synthesize controllers that achieve similar goals on different hardware platforms. While this problem can be solved with existing synthesis algorithms, current state-of-the-art tools fail to scale. To cope with the computational complexity of the problem, we introduce a special form of specification format, called {\em Separated GR($k$)}, which can be solved with a scalable synthesis algorithm but still allows for a large set of realistic specifications. We solve the realizability and the synthesis problems for Separated GR($k$), and show how to exploit the separated nature of our specification to construct better algorithms, in terms of time complexity, than known algorithms for GR($k$) synthesis. We then describe a tool, called SGR($k$), that we have implemented based on the above approach and show, by experimental evaluation, how our tool outperforms current state-of-the-art tools on various benchmarks and test-cases.

cs.FL↗

arXiv2021

A Cycle Joining Construction of the Prefer-Max De Bruijn Sequence

We propose a novel construction for the well-known prefer-max De Bruijn sequence, based on the cycle joining technique. We further show that the construction implies known results from the literature in a straightforward manner. First, it implies the correctness of the onion theorem, stating that, effectively, the reverse of prefer-max is in fact an infinite De Bruijn sequence. Second, it implies the correctness of recently discovered shift rules for prefer-max, prefer-min, and their reversals. Lastly, it forms an alternative proof for the seminal FKM-theorem.

cs.DM↗

arXiv2020

De Bruijn Sequences: From Games to Shift-Rules to a Proof of the Fredricksen-Kessler-Maiorana Theorem

We present a combinatorial game and propose efficiently computable optimal strategies. We then show how these strategies can be translated to efficiently computable shift-rules for the well known prefer-max and prefer-min De Bruijn sequences, in both forward and backward directions. Using these shift-rules, we provide a new proof of the well known theorem by Fredricksen, Kessler, and Maiorana on De Bruijn sequences and Lyndon words.

cs.DM↗

arXiv2020

Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games

$ω$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $μ$-calculus, when applied over game graphs with $ω$-regular winning conditions, allows defining symbolic algorithms in the form of fixed-point formulas for computing the sets of winning states. In this paper, we introduce energy $μ$-calculus, a multi-valued extension of the $μ$-calculus that serves as a symbolic framework for solving $ω$-regular energy games. Energy $μ$-calculus enables the seamless reuse of existing, well-known symbolic $μ$-calculus algorithms for $ω$-regular games, to solve their corresponding energy augmented variants. We define the syntax and semantics of energy $μ$-calculus over symbolic representations of the game graphs, and show how to use it to solve the decision and the minimum credit problems for $ω$-regular energy games, for both bounded and unbounded energy level accumulations.

cs.LO↗

arXiv2019

An Efficient Generalized Shift-Rule for the Prefer-Max De Bruijn Sequence

One of the fundamental ways to construct De Bruijn sequences is by using a shift-rule. A shift-rule receives a word as an argument and computes the symbol that appears after it in the sequence. An optimal shift-rule for an $(n,k)$-De Bruijn sequence runs in time $O(n)$. We propose an extended notion we name a generalized-shift-rule, which receives a word, $w$, and an integer, $c$, and outputs the $c$ symbols that comes after $w$. An optimal generalized-shift-rule for an $(n,k)$-De Bruijn sequence runs in time $O(n+c)$. We show that, unlike in the case of a shift-rule, a time optimal generalized-shift-rule allows to construct the entire sequence efficiently. We provide a time optimal generalized-shift-rule for the well-known prefer-max and prefer-min De Bruijn sequences.

cs.DM↗

arXiv2018

An Efficient Shift Rule for the Prefer-Max De Bruijn Sequence

A shift rule for the prefer-max De Bruijn sequence is formulated, for all sequence orders, and over any finite alphabet. An efficient algorithm for this shift rule is presented, which has linear (in the sequence order) time and memory complexity.

cs.DM↗

arXiv2015

The F-snapshot Problem

Aguilera, Gafni and Lamport introduced the signaling problem in [5]. In this problem, two processes numbered 0 and 1 can call two procedures: update and Fscan. A parameter of the problem is a two- variable function $F(x_0,x_1)$. Each process $p_i$ can assign values to variable $x_i$ by calling update(v) with some data value v, and compute the value: $F(x_0,x_1)$ by executing an Fscan procedure. The problem is interesting when the domain of $F$ is infinite and the range of $F$ is finite. In this case, some "access restrictions" are imposed that limit the size of the registers that the Fscan procedure can access. Aguilera et al. provided a non-blocking solution and asked whether a wait-free solution exists. A positive answer can be found in [7]. The natural generalization of the two-process signaling problem to an arbitrary number of processes turns out to yield an interesting generalization of the fundamental snapshot problem, which we call the F-snapshot problem. In this problem $n$ processes can write values to an $n$-segment array (each process to its own segment), and can read and obtain the value of an n-variable function $F$ on the array of segments. In case that the range of $F$ is finite, it is required that only bounded registers are accessed when the processes apply the function $F$ to the array, although the data values written to the segments may be taken from an infinite set. We provide here an affirmative answer to the question of Aguilera et al. for an arbitrary number of processes. Our solution employs only single-writer atomic registers, and its time complexity is $O(n \log n)$, which is also the time complexity of the fastest snapshot algorithm that uses only single-writer registers.

cs.DC↗

arXiv2015

Simple Executions of Snapshot Implementations

The well known snapshot primitive in concurrent programming allows for n-asynchronous processes to write values to an array of single-writer registers and, for each process, to take a snapshot of these registers. In this paper we provide a formulation of the well known linearizability condition for snapshot algorithms in terms of the existence of certain mathematical functions. In addition, we identify a simplifying property of snapshot implementations we call "schedule-based algorithms". This property is natural to assume in the sense that as far as we know, every published snapshot algorithm is schedule-based. Based on this, we prove that when dealing with schedule-based algorithms, it suffices to consider only a small class of very simple executions to prove or disprove correctness in terms of linearizability. We believe that the ideas developed in this paper may help to design automatic verification of snapshot algorithms. Since verifying linearizability was recently proved to be EXPSPACE-complete, focusing on unique objects (snapshot in our case) can potentially lead to designing restricted, but feasible verification methods.

cs.DC↗

arXiv2013

On the Mailbox Problem

The Mailbox Problem was described and solved by Aguilera, Gafni, and Lamport in their 2010 DC paper with an algorithm that uses two flag registers that carry 14 values each. An interesting problem that they ask is whether there is a mailbox algorithm with smaller flag values. We give a positive answer by describing a mailbox algorithm with 6 and 4 values in the two flag registers.

cs.DC↗