Symbolic Polytopes for Quantitative Interpolation and Verification
Symbolic Polytopes for Quantitative Interpolation and Verification
复制标题
用于定量插值和验证的符号多面体
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
A. Rybalchenko
中科院分区：
文献类型：
--
作者：
K. V. Gleissenthall;Boris Köpf;A. Rybalchenko
证明程序的定量属性，例如资源使用的界限或信息泄漏，通常会导致涉及集合基数的验证条件。处理此类验证条件的现有方法通过检查给定公式的基数界限来操作。然而，它们无法合成满足给定基数约束的公式，这限制了它们推断基于基数的归纳论证的适用性。
Proving quantitative properties of programs, such as bounds on resource usage or information leakage, often leads to verification conditions that involve cardinalities of sets. Existing approaches for dealing with such verification conditions operate by checking cardinality bounds for given formulas. However, they cannot synthesize formulas that satisfy given cardinality constraints, which limits their applicability for inferring cardinality-based inductive arguments.
解决存在量化的喇叭子句
DOI：
10.1007/978-3-642-39799-8_61
发表时间：
2013
期刊：
影响因子：
--
作者：
Tewodros A. Beyene;Corneliu Popeea;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko