Towards bounded model checking using nonlinear programming solver

Abstract

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.