arXiv subjects

Gera Weiss

Publications and source records attributed to Gera Weiss.

At least 19 recordsLinked to original sources

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↗

arXiv2025

A Behavior-Based Knowledge Representation Improves Prediction of Players' Moves in Chess by 25%

Predicting player behavior in strategic games, especially complex ones like chess, presents a significant challenge. The difficulty arises from several factors. First, the sheer number of potential outcomes stemming from even a single position, starting from the initial setup, makes forecasting a player's next move incredibly complex. Second, and perhaps even more challenging, is the inherent unpredictability of human behavior. Unlike the optimized play of engines, humans introduce a layer of variability due to differing playing styles and decision-making processes. Each player approaches the game with a unique blend of strategic thinking, tactical awareness, and psychological tendencies, leading to diverse and often unexpected actions. This stylistic variation, combined with the capacity for creativity and even irrational moves, makes predicting human play difficult. Chess, a longstanding benchmark of artificial intelligence research, has seen significant advancements in tools and automation. Engines like Deep Blue, AlphaZero, and Stockfish can defeat even the most skilled human players. However, despite their exceptional ability to outplay top-level grandmasters, predicting the moves of non-grandmaster players, who comprise most of the global chess community -- remains complicated for these engines. This paper proposes a novel approach combining expert knowledge with machine learning techniques to predict human players' next moves. By applying feature engineering grounded in domain expertise, we seek to uncover the patterns in the moves of intermediate-level chess players, particularly during the opening phase of the game. Our methodology offers a promising framework for anticipating human behavior, advancing both the fields of AI and human-computer interaction.

cs.LG↗

arXiv2025

Exploring and Evaluating Interplays of BPpy with Deep Reinforcement Learning and Formal Methods

We explore and evaluate the interactions between Behavioral Programming (BP) and a range of Artificial Intelligence (AI) and Formal Methods (FM) techniques. Our goal is to demonstrate that BP can serve as an abstraction that integrates various techniques, enabling a multifaceted analysis and a rich development process. Specifically, the paper examines how the BPpy framework, a Python-based implementation of BP, is enhanced by and enhances various FM and AI tools. We assess how integrating BP with tools such as Satisfiability Modulo Theory (SMT) solvers, symbolic and probabilistic model checking, and Deep Reinforcement Learning (DRL) allow us to scale the abilities of BP to model complex systems. Additionally, we illustrate how developers can leverage multiple tools within a single modeling and development task. The paper provides quantitative and qualitative evidence supporting the feasibility of our vision to create a comprehensive toolbox for harnessing AI and FM methods in a unified development framework.

cs.SE↗

arXiv2024

Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements

One of the benefits of using executable specifications such as Behavioral Programming (BP) is the ability to align the system implementation with its requirements. This is facilitated in BP by a protocol that allows independent implementation modules that specify what the system may, must, and must not do. By that, each module can enforce a single system requirement, including negative specifications such as "don't do X after Y." The existing BP protocol, however, allows only the enforcement of safety requirements and does not support the execution of liveness properties such as "do X at least three times." To model liveness requirements in BP directly and independently, we propose idioms for tagging states with "must-finish," indicating that tasks are yet to be completed. We show that this idiom allows a direct specification of known requirements patterns from the literature. We also offer semantics and two execution mechanisms, one based on a translation to B\"uchi automata and the other based on a Markov decision process (MDP). The latter approach offers the possibility of utilizing deep reinforcement learning (DRL) algorithms, which bear the potential to handle large software systems effectively. This paper presents a qualitative and quantitative assessment of the proposed approach using a proof-of-concept tool. A formal analysis of the MDP-based execution mechanism is given in an appendix.

cs.SE↗

arXiv2024

Evolving Assembly Code in an Adversarial Environment

In this work, we evolve Assembly code for the CodeGuru competition. The goal is to create a survivor -- an Assembly program that runs the longest in shared memory, by resisting attacks from adversary survivors and finding their weaknesses. For evolving top-notch solvers, we specify a Backus Normal Form (BNF) for the Assembly language and synthesize the code from scratch using Genetic Programming (GP). We evaluate the survivors by running CodeGuru games against human-written winning survivors. Our evolved programs found weaknesses in the programs they were trained against and utilized them. To push evolution further, we implemented memetic operators that utilize machine learning to explore the solution space effectively. This work has important applications for cyber-security as we utilize evolution to detect weaknesses in survivors. The Assembly BNF is domain-independent; thus, by modifying the fitness function, it can detect code weaknesses and help fix them. Finally, the CodeGuru competition offers a novel platform for analyzing GP and code evolution in adversarial environments. To support further research in this direction, we provide a thorough qualitative analysis of the evolved survivors and the weaknesses found.

cs.NE↗

arXiv2023

Provengo: A Tool Suite for Scenario Driven Model-Based Testing

We present Provengo, a comprehensive suite of tools designed to facilitate the implementation of Scenario-Driven Model-Based Testing (SDMBT), an innovative approach that utilizes scenarios to construct a model encompassing the user's perspective and the system's business value while also defining the desired outcomes. With the assistance of Provengo, testers gain the ability to effortlessly create natural user stories and seamlessly integrate them into a model capable of generating effective tests. The demonstration illustrates how SDMBT effectively addresses the bootstrapping challenge commonly encountered in model-based testing (MBT) by enabling incremental development, starting from simple models and gradually augmenting them with additional stories.

cs.SE↗

arXiv2022

Efficient One Sided Kolmogorov Approximation

We present an efficient algorithm that, given a discrete random variable $X$ and a number $m$, computes a random variable whose support is of size at most $m$ and whose Kolmogorov distance from $X$ is minimal, also for the one-sided Kolmogorov approximation. We present some variants of the algorithm, analyse their correctness and computational complexity, and present a detailed empirical evaluation that shows how they performs in practice. The main application that we examine, which is our motivation for this work, is estimation of the probability missing deadlines in series-parallel schedules. Since exact computation of these probabilities is NP-hard, we propose to use the algorithms described in this paper to obtain an approximation.

stat.ML↗

arXiv2022

What Petri Net Obliges Us to Say: Comparing Approaches for Behavior Composition

We identify and demonstrate a weakness of Petri Nets (PN) in specifying composite behavior of reactive systems. Specifically, we show how, when specifying multiple requirements in one PN model, modelers are obliged to specify mechanisms for combining these requirements. This yields, in many cases, over-specification and incorrect models. We demonstrate how some execution paths are missed, and some are generated unintentionally. To support this claim, we analyze PN models from the literature, identify the combination mechanisms, and demonstrate their effect on the correctness of the model. To address this problem, we propose to model the system behavior using behavioral programming (BP), a software development and modeling paradigm designed for seamless integration of independent requirements. Specifically, we demonstrate how the semantics of BP, which define how to interweave scenarios into a single model, allow avoiding the over-specification. Additionally, while BP maintains the same mathematical properties as PN, it provides means for changing the model dynamically, thus increasing the agility of the specification. We compare BP and PN in quantitative and qualitative measures by analyzing the models, their generated execution paths, and the specification process. Finally, while BP is supported by tools that allow for applying formal methods and reasoning techniques to the model, it lacks the legacy of PN tools and algorithms. To address this issue, we propose semantics and a tool for translating BP models to PN and vice versa.

cs.SE↗

arXiv2022

The Normalized Edit Distance with Uniform Operation Costs is a Metric

We prove that the normalized edit distance proposed in [Marzal and Vidal 1993] is a metric when the cost of all the edit operations are the same. This closes a long standing gap in the literature where several authors noted that this distance does not satisfy the triangle inequality in the general case, and that it was not known whether it is satisfied in the uniform case where all the edit costs are equal. We compare this metric to two normalized metrics proposed as alternatives in the literature, when people thought that Marzal's and Vidal's distance is not a metric, and identify key properties that explain why the original distance, now known to also be a metric, is better for some applications. Our examination is from a point of view of formal verification, but the properties and their significance are stated in an application agnostic way.

cs.FL↗

arXiv2022

Generalized Coverage Criteria for Combinatorial Sequence Testing

We present a new model-based approach for testing systems that use sequences of actions and assertions as test vectors. Our solution includes a method for quantifying testing quality, a tool for generating high-quality test suites based on the coverage criteria we propose, and a framework for assessing risks. For testing quality, we propose a method that specifies generalized coverage criteria over sequences of actions, which extends previous approaches. Our publicly available tool demonstrates how to extract effective test suites from test plans based on these criteria. We also present a Bayesian approach for measuring the probabilities of bugs or risks, and show how this quantification can help achieve an informed balance between exploitation and exploration in testing. Finally, we provide an empirical evaluation demonstrating the effectiveness of our tool in finding bugs, assessing risks, and achieving coverage.

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↗

arXiv2019

On-the-Fly Construction of Composite Events in Scenario-Based Modeling using Constraint Solvers

Scenario-Based Programming is a methodology for modeling and constructing complex reactive systems from simple, stand-alone building blocks, called scenarios. These scenarios are designed to model different traits of the system, and can be interwoven together and executed to produce cohesive system behavior. Existing execution frameworks for scenario-based programs allow scenarios to specify their view of what the system must, may, or must not do only through very strict interfaces. This limits the methodology's expressive power and often prevents users from modeling certain complex requirements. Here, we propose to extend Scenario-Based Programming's execution mechanism to allow scenarios to specify how the system should behave using rich logical constraints. We then leverage modern constraint solvers (such as SAT or SMT solvers) to resolve these constraints at every step of running the system, towards yielding the desired overall system behavior. We provide an implementation of our approach and demonstrate its applicability to various systems that could not be easily modeled in an executable manner by existing Scenario-Based approaches.

cs.SE↗

arXiv2019

Onion De Bruijn Sequences: Fixed-Window Counting by Growing the Alphabet

We study a fixed-window counting system in which integers are represented by words of constant length while the alphabet grows as needed. This viewpoint arises from De Bruijn sequences: for fixed order $n$, the reverse prefer-max sequence is compatible with alphabet growth, since for each $k$ its restriction to $[k]^n$ is a De Bruijn sequence, yielding an infinite sequence over $\mathbb{N}$. We formalize this through the notion of an onion De Bruijn sequence, prove the resulting structural properties, and count compatible finite onion prefixes by an explicit product formula. For orders $n=2,3$, we give explicit rank and unrank formulas and describe addition and multiplication via finite normalization, with exact carry counts and linear carry complexity in the input layers.

cs.DM↗

arXiv2018

BPjs --- a framework for modeling reactive systems using a scripting language and BP

We describe some progress towards a new common framework for model driven engineering, based on behavioral programming. The tool we have developed unifies almost all of the work done in behavioral programming so far, under a common set of interfaces. Its architecture supports pluggable event selection strategies, which can make models more intuitive and compact. Program state space can be traversed using various algorithms, such as DFS and A*. Furthermore, program state is represented in a way that enables scanning a state space using parallel and distributed algorithms. Executable models created with this tool can be directly embedded in Java applications, enabling a model-first approach to system engineering, where initially a model is created and verified, and then a working application is gradually built around the model. The model itself consists of a collection of small scripts written in JavaScript (hence "BPjs"). Using a variety of case-studies, this paper shows how the combination of a lenient programming language with formal model analysis tools creates an efficient way of developing robust complex systems. Additionally, as we learned from an experimental course we ran, the usage of JavaScript make practitioners more amenable to using this system and, thus, model checking and model driven engineering. In addition to providing infrastructure for development and case-studies in behavioral programming, the tool is designed to serve as a common platform for research and innovation in behavioral programming and in model driven engineering in general.

cs.SE↗

arXiv2018

An optimal approximation of discrete random variables with respect to the Kolmogorov distance

We present an algorithm that takes a discrete random variable $X$ and a number $m$ and computes a random variable whose support (set of possible outcomes) is of size at most $m$ and whose Kolmogorov distance from $X$ is minimal. In addition to a formal theoretical analysis of the correctness and of the computational complexity of the algorithm, we present a detailed empirical evaluation that shows how the proposed approach performs in practice in different applications and domains.

cs.DS↗

arXiv2018

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↗