Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware and software verification. They are rooted in the Boolean setting and are successful for, e.g., first-order theories such as linear rational arithmetic. What about their applicability in the quantitative setting where formulae evaluate to numbers and quantitative supremum/infimum quantifiers are the natural counterparts of Boolean quantifiers? Applications include establishing quantitative properties of programs, such as bounds on expected outcomes of probabilistic programs featuring nondeterminism, and analyzing the flow of information through programs. In this paper, we present, to the best of our knowledge, the first QE algorithm for possibly unbounded, $\infty$- or $-\infty$-valued, or discontinuous piecewise linear quantities. They are the quantitative counterpart to linear rational arithmetic, and they are a popular quantitative assertion language for probabilistic program verification. We provide rigorous soundness proofs as well as upper space complexity bounds. Moreover, we present two applications of our QE algorithm. First, our algorithm yields a quantitative CI theorem: given arbitrary piecewise linear quantities $f$ and $g$ with $f \models g$, both the strongest and the weakest Craig interpolant of $f$ and $g$ are quantifier-free and effectively constructible. Second, we apply our QE algorithm to compute minimal and maximal expected outcomes of loop-free probabilistic programs featuring unbounded nondeterminism.

翻译：量词消解（QE）与Craig插值（CI）是当前硬件与软件验证自动化方法的核心技术。它们源于布尔逻辑背景，并在线性有理算术等一阶理论中取得显著成功。那么在定量场景中——公式求值结果为数值，且定量上确界/下确界量词成为布尔量词的自然对应物——它们的适用性如何？该场景的应用包括：建立程序的定量性质（例如含非确定性的概率程序期望结果边界），以及分析程序中的信息流。本文首次提出了适用于可能无界、取值$\infty$或$-\infty$、或不连续的分段线性量的QE算法。这类量是线性有理算术的定量对应形式，也是概率程序验证中广泛使用的定量断言语言。我们提供了严格的正确性证明及空间复杂度上界分析。此外，本文展示了QE算法的两项应用：首先，该算法可推导出定量CI定理——对于满足$f \models g$的任意分段线性量$f$和$g$，其最强与最弱Craig插值均为可有效构造的无量词公式；其次，我们将QE算法应用于计算含无界非确定性的无循环概率程序的最小与最大期望结果。