A common approach to solving problems in the sciences is to reduce them to solving some kind of system of equations. While in engineering and physics those systems often involve quantities over the reals, computer science predominantly deals with discrete domains such as the integers. However, performing arithmetic over the integers is computationally expensive, affecting both decidability and complexity. In some cases, solutions even grow too large to be explicitly constructed.

This talk will survey recent results and techniques for deciding integer logics, even when solutions are prohibitively large to construct explicitly. In more technical terms, I will outline how we can establish an NP upper bound for existential Büchi arithmetic and an EXPSPACE upper bound for existential Semenov arithmetic, using techniques from automata theory and specifically vector addition systems. The talk is aimed at a broad audience and assumes no prior knowledge of these logics. I will also discuss applications, particularly in solving restricted classes of string constraints.

Market fragmentation across multiple Automated Market Makers (AMMs) creates inefficiencies such as costly arbitrage, unnecessarily high slippage and delayed incorporation of new information into prices. These inefficiencies raise trading costs, reduce liquidity provider profits, and degrade overall market efficiency. To address these issues, we propose a modification of the Constant Product Market Maker (CPMM) pricing mechanism, called the Global Market Maker (GMM), which aggregates liquidity information from all AMMs to mitigate these inefficiencies. Through theoretical and numerical analyses, we demonstrate that the GMM enhances profits for both AMMs and traders by eliminating arbitrage opportunities. Additionally, it reduces the profitability of sandwich attacks and minimizes impermanent losses.

The dominant guiding philosophy in the first sixty years of Computer Science was for designers to design systems that were always correct, and to accept nothing less as users. But times have changed: Users and designers are accustomed to systems with statistical components and behaviors. What does it mean for the formal methods community? In this talk, we argue that such a dramatic change in the acceptance and design of systems presents exciting opportunities to make fundamental contributions: we need to rethink the notions and techniques for the design of specifications and verification methodologies. In particular, we will focus on the systems whose behaviors are not naturally captured by symbolic relations but rather require reliance on probability distributions. We will discuss our recent efforts in designing formal methodologies for testing whether a sampling subroutine generates a desired distribution. We will showcase the challenges, opportunities, and rewards in our journey.

Reasoning about hyperproperties of concurrent implementations, such as the guarantees these implementations provide to randomized client programs, has been a long-standing challenge. Standard linearizability enables the use of atomic specifications for reasoning about standard properties, but not about hyperproperties. A stronger correctness criterion, called strong linearizability, enables such reasoning, but is rarely achievable, leaving various useful implementations with no means for reasoning about their hyperproperties. In this paper, we focus on registers and devise non-atomic specifications that capture a wide-range of well-studied register implementations and enable reasoning about their hyperproperties. First, we consider the class of write strong-linearizable implementations, a recently proposed useful weakening of strong linearizability, which allows more implementations, such as the well-studied single-writer ABD distributed implementation. We introduce a simple shared-memory register specification that can be used for reasoning about hyperproperties of programs that use write strongly-linearizable implementations. Second, we introduce a new linearizability class, which we call decisive linearizability, that is weaker than write strong-linearizability and includes multi-writer ABD, and develop a second shared-memory register specification for reasoning about hyperproperties of programs that use register implementations of this class. These results shed light on the hyperproperties guaranteed when simulating shared memory in a crash-resilient message-passing system.

Based on joint work with Yoav Ben Shimon and Sharon Shoham presented as DISC'24.

Byzantine agreement, a fundamental problem in distributed computing, enables $N$ processes to reach consensus on a common value despite up to $T < N$ arbitrary failures. It serves as the backbone of critical distributed services such as distributed key generation (DKG), secure multi-party computation (MPC), blockchain technologies, and state machine replication (SMR), highlighting its crucial role in modern computing. Despite their importance, existing agreement protocols face significant limitations. Many struggle to scale efficiently due to poor performance or heavy reliance on cryptographic tools such as threshold signatures, which require expensive setup and computationally intensive algebraic operations. Furthermore, dependence on these “heavyweight” cryptographic primitives weakens their security in a post-quantum world. As agreement protocols continue to grow in scale and importance, there is an urgent need for solutions that are both efficient and resilient to emerging security threats and future technological advancements. In this talk, I will present the first complexity-optimal agreement protocols that either rely only on “lightweight” cryptographic primitives, such as hash functions, or eliminate the need for cryptography entirely. These solutions cover all major network models— asynchrony, partial synchrony, and synchrony—matching or exceeding the best-known results while relying on minimal cryptographic assumptions.