arXiv subjects

Orna Grumberg

Publications and source records attributed to Orna Grumberg.

6 recordsLinked to original sources

arXiv2026

Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning

Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors ($\mathcal{T}_B$) is fundamental to bit-precise program verification. However, state-of-the-art CHC-solvers often struggle with $\mathcal{T}_B$, limiting scalability in bit-precise reasoning. We present Mosaic, a theory-modular framework for deciding satisfiability of CHCs modulo $\mathcal{T}_B$ by combining reasoning in $\mathcal{T}_B$ and the theory of Integer Arithmetic ($\mathcal{T}_I$). Given a CHC set modulo $\mathcal{T}_B$, Mosaic partitions it into two fragments interpreted over $\mathcal{T}_B$ and $\mathcal{T}_I$. Moreover, it implements an algorithm that reasons about the fragments in a modular fashion, exchanges information between them via sound translations across theories, and determines satisfiability w.r.t. the original CHC set. We implemented a prototype of Mosaic using Z3 and Spacer and evaluated it on bit-manipulating benchmarks. Our evaluation shows that Mosaic significantly outperforms Spacer on these benchmarks.

cs.LO↗

arXiv2025

STACHE: Local Black-Box Explanations for Reinforcement Learning Policies

Reinforcement learning agents often behave unexpectedly in sparse-reward or safety-critical environments, creating a strong need for reliable debugging and verification tools. In this paper, we propose STACHE, a comprehensive framework for generating local, black-box explanations for an agent's specific action within discrete Markov games. Our method produces a Composite Explanation consisting of two complementary components: (1) a Robustness Region, the connected neighborhood of states where the agent's action remains invariant, and (2) Minimal Counterfactuals, the smallest state perturbations required to alter that decision. By exploiting the structure of factored state spaces, we introduce an exact, search-based algorithm that circumvents the fidelity gaps of surrogate models. Empirical validation on Gymnasium environments demonstrates that our framework not only explains policy actions, but also effectively captures the evolution of policy logic during training - from erratic, unstable behavior to optimized, robust strategies - providing actionable insights into agent sensitivity and decision boundaries.

cs.LG↗

arXiv2024

CTL* Verification and Synthesis using Existential Horn Clauses

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs). $CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems. EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness. We develop the translation system \textit{Trans}, which given a verification problem consisting of a program $P$ and a specification $\phi$, builds a set of EHCs which is satisfiable iff $P$ satisfies $\phi$. We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given $CTL^*$ specification. We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for $CTL^*$ verification and synthesis.

cs.LO↗

arXiv2022

Assume, Guarantee or Repair -- A Regular Framework for Non Regular Properties (full version)

We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs.

cs.FL↗

arXiv2021

Modular Verification of Concurrent Programs via Sequential Model Checking

This work utilizes the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We reduce the verification of a concurrent program to a series of verification tasks of sequential programs. Our approach is modular in the sense that each sequential verification task roughly corresponds to the verification of a single thread, with some additional information about the environment in which it operates. Information regarding the environment is gathered during the run of the algorithm, by need. While our approach is general, it specializes on concurrent programs where the threads are structured hierarchically. The idea is to exploit the hierarchy in order to minimize the amount of information that needs to be transferred between threads. To that end, we verify one of the threads, considered "main", as a sequential program. Its verification process initiates queries to its "environment" (which may contain multiple threads). Those queries are answered by sequential verification, if the environment consists of a single thread, or, otherwise, by applying the same hierarchical algorithm on the environment. Our technique is fully automatic, and allows us to use any off-the-shelf sequential model checker. We implemented our technique in a tool called CoMuS and evaluated it against established tools for concurrent verification. Our experiments show that it works particularly well on hierarchically structured programs.

cs.PL↗

arXiv2017

Formal Black-Box Analysis of Routing Protocol Implementations

The Internet infrastructure relies entirely on open standards for its routing protocols. However, the majority of routers on the Internet are closed-source. Hence, there is no straightforward way to analyze them. Specifically, one cannot easily identify deviations of a router's routing functionality from the routing protocol's standard. Such deviations (either deliberate or inadvertent) are particularly important to identify since they may degrade the security or resiliency of the network. A model-based testing procedure is a technique that allows to systematically generate tests based on a model of the system to be tested; thereby finding deviations in the system compared to the model. However, applying such an approach to a complex multi-party routing protocol requires a prohibitively high number of tests to cover the desired functionality. We propose efficient and practical optimizations to the model-based testing procedure that are tailored to the analysis of routing protocols. These optimizations allow to devise a formal black-box method to unearth deviations in closed-source routing protocols' implementations. The method relies only on the ability to test the targeted protocol implementation and observe its output. Identification of the deviations is fully automatic. We evaluate our method against one of the complex and widely used routing protocols on the Internet -- OSPF. We search for deviations in the OSPF implementation of Cisco. Our evaluation identified numerous significant deviations that can be abused to compromise the security of a network. The deviations were confirmed by Cisco. We further employed our method to analyze the OSPF implementation of the Quagga Routing Suite. The analysis revealed one significant deviation. Subsequent to the disclosure of the deviations some of them were also identified by IBM, Lenovo and Huawei in their own products.

cs.CR↗