A Mixed Real and Floating-Point Solver
A Mixed Real and Floating-Point Solver
复制标题
混合实数和浮点求解器
DOI：
10.1007/978-3-030-20652-9_25
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Rakamaric, Z.
中科院分区：
文献类型：
--
作者：
Salvia, R.;Titolo, L.;Feliu, M.A.;Moscato, M.M.;Munoz, C.A.;Rakamaric, Z.
推理混合实数和浮点约束对于开发浮点程序的精确分析工具至关重要。本文介绍了 FPRoCK，一种用于求解混合实数和浮点公式的原型工具。 FPRoCK 将混合公式转换为实数上可等满足的公式。然后使用现成的 SMT 求解器求解该公式。 FPRoCK 还与 PRECiSA 静态分析器集成，后者可以计算浮点程序舍入误差的合理估计。它用于检测不可行的计算路径，从而提高 PRECiSA 的准确性。
Reasoning about mixed real and floating-point constraints is essential for developing accurate analysis tools for floating-point programs. This paper presents FPRoCK, a prototype tool for solving mixed real and floating-point formulas. FPRoCK transforms a mixed formula into an equisatisfiable one over the reals. This formula is then solved using an off-the-shelf SMT solver. FPRoCK is also integrated with the PRECiSA static analyzer, which computes a sound estimation of the round-off error of a floating-point program. It is used to detect infeasible computational paths, thereby improving the accuracy of PRECiSA.
浮点程序舍入误差分析的抽象解释框架
DOI：
--
发表时间：
2018
期刊：
International Conference on Verification, Model Checking and Abstract Interpretation
影响因子：
--
作者：
Laura Titolo;Marco A. Feliú;Mariano M. Moscato;C. Muñoz
通讯作者：
C. Muñoz
消除浮点程序中的不稳定测试
DOI：
--
发表时间：
2018
期刊：
International Workshop/Symposium on Logic-based Program Synthesis and Transformation
影响因子：
--
作者：
Laura Titolo;C. Muñoz;Marco A. Feliú;Mariano M. Moscato
通讯作者：
Mariano M. Moscato
使用 UppSAT 探索浮点运算的近似值
DOI：
--
发表时间：
2017
期刊：
International Joint Conference on Automated Reasoning
影响因子：
--
作者：
Aleksandar Zeljić;Peter Backeman;C. Wintersteiger;Philipp Rümmer
通讯作者：
Philipp Rümmer