35 citations · 39 across the 6 of their papers we have counts for
6 papers
Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning
Omer Rappoport, Orna Grumberg, Yakir Vizel
Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors () is fundamental to bit-precise program verification. However…
STACHE: Local Black-Box Explanations for Reinforcement Learning Policies
Andrew Elashkin, Orna Grumberg
Reinforcement learning agents often behave unexpectedly in sparse-reward or safety-critical environments, creating a strong need for reliable debugging and verification tools. In t…
CTL* Verification and Synthesis using Existential Horn Clauses
Mishel Carelli, Orna Grumberg
This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to specifications, based on translation to E…
Modular Verification of Concurrent Programs via Sequential Model Checking
Dan Rasin, Orna Grumberg, Sharon Shoham
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…
Formal Black-Box Analysis of Routing Protocol Implementations
Adi Sosnovich, Orna Grumberg, Gabi Nakibly
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 stra…
Learning to Order BDD Variables in Verification
O. Grumberg, S. Livne, S. Markovitch
The size and complexity of software and hardware systems have significantly increased in the past years. As a result, it is harder to guarantee their correct behavior. One of the m…