Towards bounded model checking using nonlinear programming solver
Towards bounded model checking using nonlinear programming solver
复制标题
DOI：
10.1145/2970276.2970319
复制
发表时间：
2016-08
期刊：
影响因子：
--
通讯作者：
Masataka Nishi
中科院分区：
文献类型：
--
作者：
Masataka Nishi
由于它们的复杂性，目前可用的基于布尔可满足性和可满足性模理论的有界模型检测技术不足以处理非线性浮点和整数运算。使用数值方法，我们减少了一个有界模型检测问题的约束满足问题。目前可用的技术试图解决约束问题，但不能保证全局收敛性和正确性。使用IPOPT和ANTIGONE非线性规划（NLP）求解器，我们将原来的约束满足问题从一个有分离的约束到一个有连接的约束与一些辅助变量。该转换降低了计算成本，并保留了原问题的布尔结构，同时符合限制的NLP求解器。
Due to their complexity, currently available bounded model checking techniques based on Boolean Satisfiability and Satisfiability Modulo Theories inadequately handle non-linear floating-point and integer arithmetic. Using a numerical approach, we reduce a bounded model checking problem to a constraint satisfaction problem. Currently available techniques attempt to solve the constraint problem but can guarantee neither global convergence nor correctness. Using the IPOPT and ANTIGONE non-linear programming (NLP) solvers, we transform the original constraint satisfaction problem from one having disjunctions of constraints into one having conjunctions of constraints with a few introduced auxiliary variables. The transformation lowers the computing cost and preserves the Boolean structure of the original problem while complying with limits of NLP solvers.