arXiv subjects

Neta Elad

Publications and source records attributed to Neta Elad.

6 recordsLinked to original sources

arXiv2026

Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property

Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize symbolic structures to use any base theory that admits a standard model. Symbolic structures induce a symbolic model property, which holds for a fragment of first-order logic if every satisfiable formula in the fragment has a symbolic model. The symbolic model property implies decidability, since the model-checking problem for symbolic structures is decidable. We use the symbolic model property to prove decidability for several fragments that extend the fragment of stratified formulas, relaxing the quantifier-alternation constraints by allowing one sort to have self-looping functions, under certain restrictions. To establish the symbolic model property for these fragments we construct a symbolic model for a formula from an arbitrary model. The construction and its correctness are proved in a generic fashion, which may be instantiated to other similarly restricted fragments.

cs.LO↗

arXiv2026

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings

We present a unified deductive verification framework for first-order temporal properties based on well-founded rankings, where verification conditions are discharged using SMT solvers. To that end, we introduce a novel reduction from verification of arbitrary temporal properties to verification of termination. Our reduction augments the system with prophecy timer variables that predict the number of steps along a trace until the next time certain temporal formulas, including the negated property, hold. In contrast to standard tableaux-based reductions, which reduce the problem to fair termination, our reduction does not introduce fairness assumptions. To verify termination of the augmented system, we follow the traditional approach of assigning each state a rank from a well-founded set and showing that the rank decreases in every transition. We leverage the recently proposed formalism of implicit rankings to express and automatically verify the decrease of rank using SMT solvers, even when the rank is not expressible in first-order logic. We extend implicit rankings from finite to infinite domains, enabling verification of more general systems and making them applicable to the augmented systems generated by our reduction, which allows us to exploit the decrease of timers in termination proofs. We evaluate our technique on a range of temporal verification tasks from previous works, giving simple, intuitive proofs for them within our framework.

cs.LO↗

arXiv2025

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions

For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and permissions. Separation Logic is often extended to include inductively-defined predicates, interpreted as least fixpoints, forming Separation Logic with Inductive Definitions (SLID). Many theoretical and practical advances have been made in developing automated proof mechanisms for SLID, but these mechanisms are imperfect, and a deeper understanding of their failures is desired. As expressive as Separation Logic is, it is not surprising that it is incomplete, and in fact, it contains several sources of incompleteness that defy automated reasoning. In this paper we study these sources of incompleteness and how they relate to failures of proof mechanisms. We place SLID within a larger logic, that we call Weak Separation Logic (WSL). We prove that unlike SLID, WSL is complete for a non-trivial fragment of quantified entailments with background theories and inductive definitions, via a reduction to first-order logic (FOL). Moreover, we show that the ubiquitous fold/unfold proof mechanism is sound and complete for theory-free, quantifier-free WSL entailments with inductive definitions. Through this, we understand proof failures as stemming from nonstandard models present in WSL, but not allowed in SLID. These rogue models are typically infinite, and we use the formalism of symbolic structures to represent and automatically find them. We present a prototype tool that implements the FOL encoding of WSL and test it on an existing benchmark, which contains over 700 quantified entailment problems with inductive definitions. Our tool is able to find counter-models to many of the examples, and we provide a partial taxonomy of the rogue models, shedding some light on real-world proof failures.

cs.LO↗

arXiv2024

Axe 'Em: Eliminating Spurious States with Induction Axioms

First-order logic (FOL) has proved to be a versatile and expressive tool as the basis of abstract modeling languages. Used to verify complex systems with unbounded domains, such as heap-manipulating programs and distributed protocols, FOL, and specifically uninterpreted functions and quantifiers, strike a balance between expressiveness and amenity to automation. However, FOL semantics may differ in important ways from the intended semantics of the modeled system, due to the inability to distinguish between finite and infinite first-order structures, for example, or the undefinability of well-founded relations in FOL. This semantic gap may give rise to spurious states and unreal behaviors, which only exist as an artifact of the first-order abstraction and impede the verification process. In this paper we take a step towards bridging this semantic gap. We present an approach for soundly refining the first-order abstraction according to either well-founded semantics or finite-domain semantics, utilizing induction axioms for an abstract order relation, a common primitive in verification. We first formalize sound axiom schemata for each of the aforementioned semantics, based on well-founded induction. Second, we show how to use spurious counter-models, which are necessarily infinite, to guide the instantiation of these axiom schemata. Finally, we present a sound and complete reduction of well-founded semantics and finite-domain semantics to standard semantics in the recently discovered Ordered Self-Cycle (OSC) fragment of FOL, and prove that satisfiability under these semantics is decidable in OSC. We implement a prototype tool to evaluate our approach, and test it on various examples where spurious models arise. Our tool quickly finds the necessary axioms to refine the semantics, and successfully completes the verification process.

cs.PL↗

arXiv2023

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification

First-order logic, and quantifiers in particular, are widely used in deductive verification. Quantifiers are essential for describing systems with unbounded domains, but prove difficult for automated solvers. Significant effort has been dedicated to finding quantifier instantiations that establish unsatisfiability, thus ensuring validity of a system's verification conditions. However, in many cases the formulas are satisfiable: this is often the case in intermediate steps of the verification process. For such cases, existing tools are limited to finding finite models as counterexamples. Yet, some quantified formulas are satisfiable but only have infinite models. Such infinite counter-models are especially typical when first-order logic is used to approximate inductive definitions such as linked lists or the natural numbers. The inability of solvers to find infinite models makes them diverge in these cases. In this paper, we tackle the problem of finding such infinite models. These models allow the user to identify and fix bugs in the modeling of the system and its properties. Our approach consists of three parts. First, we introduce symbolic structures as a way to represent certain infinite models. Second, we describe an effective model finding procedure that symbolically explores a given family of symbolic structures. Finally, we identify a new decidable fragment of first-order logic that extends and subsumes the many-sorted variant of EPR, where satisfiable formulas always have a model representable by a symbolic structure within a known family. We evaluate our approach on examples from the domains of distributed consensus protocols and of heap-manipulating programs. Our implementation quickly finds infinite counter-models that demonstrate the source of verification failures in a simple way, while SMT solvers and theorem provers such as Z3, cvc5, and Vampire diverge.

cs.LO↗

arXiv2021

Summing Up Smart Transitions

Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances. Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length. In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts.

cs.LO↗