skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


This content will become publicly available on July 21, 2026

Title: Infinite-State Liveness Checking with rlive
Abstract is a recently-proposed SAT-based liveness model checking algorithm that showed remarkable performance compared to other state-of-the-art approaches, both in absolute terms (solving more problems overall than other engines on standard benchmark sets) as well as in relative terms (solving several problems that none of the other engines could solve). proves or disproves properties of the formFGq, by trying to show that$$\lnot q$$ ¬ q can be visited only a finite number of times via an incremental reduction to a sequence of reachability queries. A key factor in the good performance of is the extraction of “shoals” from the inductive invariants of the reachability queries to block states that can reach$$\lnot q$$ ¬ q a bounded number of times. In this paper, we generalize to handle infinite-state systems, using the Verification Modulo Theories paradigm. In contrast to the finite-state case, liveness cannot be simply reduced to finding a bound on the number of occurrences of$$\lnot q$$ ¬ q on paths. We propose therefore a solution leveraging predicate abstraction and termination techniques based on well-founded relations. In particular, we show how we can extract shoals that take into account the well-founded relations. We implemented the technique on top of the open source VMT engine IC3ia and we experimentally demonstrate how the new extension maintains the performance advantages (both absolute and relative) of the original , thus significantly contributing to advancing the state of the art of infinite-state liveness verification.  more » « less
Award ID(s):
2038903 2016592
PAR ID:
10648930
Author(s) / Creator(s):
; ; ; ;
Publisher / Repository:
Springer Nature Switzerland
Date Published:
Page Range / eLocation ID:
215 to 236
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Abstract Despite the f0(980) hadron having been discovered half a century ago, the question about its quark content has not been settled: it might be an ordinary quark-antiquark ($${{\rm{q}}}\overline{{{\rm{q}}}}$$ q q ¯ ) meson, a tetraquark ($${{\rm{q}}}\overline{{{\rm{q}}}}{{\rm{q}}}\overline{{{\rm{q}}}}$$ q q ¯ q q ¯ ) exotic state, a kaon-antikaon ($${{\rm{K}}}\overline{{{\rm{K}}}}$$ K K ¯ ) molecule, or a quark-antiquark-gluon ($${{\rm{q}}}\overline{{{\rm{q}}}}{{\rm{g}}}$$ q q ¯ g ) hybrid. This paper reports strong evidence that the f0(980) state is an ordinary$${{\rm{q}}}\overline{{{\rm{q}}}}$$ q q ¯ meson, inferred from the scaling of elliptic anisotropies (v2) with the number of constituent quarks (nq), as empirically established using conventional hadrons in relativistic heavy ion collisions. The f0(980) state is reconstructed via its dominant decay channel f0(980) →π+π, in proton-lead collisions recorded by the CMS experiment at the LHC, and itsv2is measured as a function of transverse momentum (pT). It is found that thenq= 2 ($${{\rm{q}}}\overline{{{\rm{q}}}}$$ q q ¯ state) hypothesis is favored overnq= 4 ($${{\rm{q}}}\overline{{{\rm{q}}}}{{\rm{q}}}\overline{{{\rm{q}}}}$$ q q ¯ q q ¯ or$${{\rm{K}}}\overline{{{\rm{K}}}}$$ K K ¯ states) by 7.7, 6.3, or 3.1 standard deviations in thepT< 10, 8, or 6 GeV/cranges, respectively, and overnq= 3 ($${{\rm{q}}}\overline{{{\rm{q}}}}{{\rm{g}}}$$ q q ¯ g hybrid state) by 3.5 standard deviations in thepT< 8 GeV/crange. This result represents the first determination of the quark content of the f0(980) state, made possible by using a novel approach, and paves the way for similar studies of other exotic hadron candidates. 
    more » « less
  2. Abstract We consider integral area-minimizing 2-dimensional currents$$T$$ T in$$U\subset \mathbf {R}^{2+n}$$ U R 2 + n with$$\partial T = Q\left [\!\![{\Gamma }\right ]\!\!]$$ T = Q Γ , where$$Q\in \mathbf {N} \setminus \{0\}$$ Q N { 0 } and$$\Gamma $$ Γ is sufficiently smooth. We prove that, if$$q\in \Gamma $$ q Γ is a point where the density of$$T$$ T is strictly below$$\frac{Q+1}{2}$$ Q + 1 2 , then the current is regular at$$q$$ q . The regularity is understood in the following sense: there is a neighborhood of$$q$$ q in which$$T$$ T consists of a finite number of regular minimal submanifolds meeting transversally at$$\Gamma $$ Γ (and counted with the appropriate integer multiplicity). In view of well-known examples, our result is optimal, and it is the first nontrivial generalization of a classical theorem of Allard for$$Q=1$$ Q = 1 . As a corollary, if$$\Omega \subset \mathbf {R}^{2+n}$$ Ω R 2 + n is a bounded uniformly convex set and$$\Gamma \subset \partial \Omega $$ Γ Ω a smooth 1-dimensional closed submanifold, then any area-minimizing current$$T$$ T with$$\partial T = Q \left [\!\![{\Gamma }\right ]\!\!]$$ T = Q Γ is regular in a neighborhood of $$\Gamma $$ Γ
    more » « less
  3. Abstract Given a prime powerqand$$n \gg 1$$ n 1 , we prove that every integer in a large subinterval of the Hasse–Weil interval$$[(\sqrt{q}-1)^{2n},(\sqrt{q}+1)^{2n}]$$ [ ( q - 1 ) 2 n , ( q + 1 ) 2 n ] is$$\#A({\mathbb {F}}_q)$$ # A ( F q ) for some ordinary geometrically simple principally polarized abelian varietyAof dimensionnover$${\mathbb {F}}_q$$ F q . As a consequence, we generalize a result of Howe and Kedlaya for$${\mathbb {F}}_2$$ F 2 to show that for each prime powerq, every sufficiently large positive integer is realizable, i.e.,$$\#A({\mathbb {F}}_q)$$ # A ( F q ) for some abelian varietyAover$${\mathbb {F}}_q$$ F q . Our result also improves upon the best known constructions of sequences of simple abelian varieties with point counts towards the extremes of the Hasse–Weil interval. A separate argument determines, for fixedn, the largest subinterval of the Hasse–Weil interval consisting of realizable integers, asymptotically as$$q \rightarrow \infty $$ q ; this gives an asymptotically optimal improvement of a 1998 theorem of DiPippo and Howe. Our methods are effective: We prove that if$$q \le 5$$ q 5 , then every positive integer is realizable, and for arbitraryq, every positive integer$$\ge q^{3 \sqrt{q} \log q}$$ q 3 q log q is realizable. 
    more » « less
  4. Abstract Let$$\mathbb {F}_q^d$$ F q d be thed-dimensional vector space over the finite field withqelements. For a subset$$E\subseteq \mathbb {F}_q^d$$ E F q d and a fixed nonzero$$t\in \mathbb {F}_q$$ t F q , let$$\mathcal {H}_t(E)=\{h_y: y\in E\}$$ H t ( E ) = { h y : y E } , where$$h_y:E\rightarrow \{0,1\}$$ h y : E { 0 , 1 } is the indicator function of the set$$\{x\in E: x\cdot y=t\}$$ { x E : x · y = t } . Two of the authors, with Maxwell Sun, showed in the case$$d=3$$ d = 3 that if$$|E|\ge Cq^{\frac{11}{4}}$$ | E | C q 11 4 andqis sufficiently large, then the VC-dimension of$$\mathcal {H}_t(E)$$ H t ( E ) is 3. In this paper, we generalize the result to arbitrary dimension by showing that the VC-dimension of$$\mathcal {H}_t(E)$$ H t ( E ) isdwhenever$$E\subseteq \mathbb {F}_q^d$$ E F q d with$$|E|\ge C_d q^{d-\frac{1}{d-1}}$$ | E | C d q d - 1 d - 1
    more » « less
  5. Abstract Schinzel and Wójcik have shown that for every$$\alpha ,\beta \in \mathbb {Q}^{\times }\hspace{0.55542pt}{\setminus }\hspace{1.111pt}\{\pm 1\}$$ α , β Q × \ { ± 1 } , there are infinitely many primespwhere$$v_p(\alpha )=v_p(\beta )=0$$ v p ( α ) = v p ( β ) = 0 and where$$\alpha $$ α and$$\beta $$ β generate the same multiplicative group modp. We prove a weaker result in the same direction for algebraic numbers$$\alpha , \beta $$ α , β . Let$$\alpha , \beta \in \overline{\mathbb {Q}} ^{\times }$$ α , β Q ¯ × , and suppose$$|N_{\mathbb {Q}(\alpha ,\beta )/\mathbb {Q}}(\alpha )|\ne 1$$ | N Q ( α , β ) / Q ( α ) | 1 and$$|N_{\mathbb {Q}(\alpha ,\beta )/\mathbb {Q}}(\beta )|\ne 1$$ | N Q ( α , β ) / Q ( β ) | 1 . Then for some positive integer$$C = C(\alpha ,\beta )$$ C = C ( α , β ) , there are infinitely many prime idealsPof Equation missing<#comment/>where$$v_P(\alpha )=v_P(\beta )=0$$ v P ( α ) = v P ( β ) = 0 and where the group$$\langle \beta \bmod {P}\rangle $$ β mod P is a subgroup of$$\langle \alpha \bmod {P}\rangle $$ α mod P with$$[\langle \alpha \bmod {P}\rangle \,{:}\, \langle \beta \bmod {P}\rangle ]$$ [ α mod P : β mod P ] dividingC. A key component of the proof is a theorem of Corvaja and Zannier bounding the greatest common divisor of shiftedS-units. 
    more » « less