TY - GEN
T1 - OptCE: A Counterexample-Guided Inductive Optimization Solver
AU - Albuquerque, Higo F.
AU - Araújo, Rodrigo F.
AU - Bessa, Iury V.
AU - Cordeiro, Lucas C.
AU - De Lima Filho, Eddie B.
PY - 2017
Y1 - 2017
N2 - This paper presents optimization through counterexamples (OptCE), which is a verification tool developed for optimizing target functions. In particular, OptCE employs bounded model checking techniques based on boolean satisfiability and satisfiability modulo theories, which are able to obtain global minima of convex and non-convex functions. OptCE is implemented in C/C ++++ , performs all optimization steps automatically, and iteratively analyzes counterexamples, in order to inductively achieve global optimization based on a verification oracle. Experimental results show that OptCE can effectively find optimal solutions for all evaluated benchmarks, while traditional techniques are usually trapped by local minima.
AB - This paper presents optimization through counterexamples (OptCE), which is a verification tool developed for optimizing target functions. In particular, OptCE employs bounded model checking techniques based on boolean satisfiability and satisfiability modulo theories, which are able to obtain global minima of convex and non-convex functions. OptCE is implemented in C/C ++++ , performs all optimization steps automatically, and iteratively analyzes counterexamples, in order to inductively achieve global optimization based on a verification oracle. Experimental results show that OptCE can effectively find optimal solutions for all evaluated benchmarks, while traditional techniques are usually trapped by local minima.
U2 - 10.1007/978-3-319-70848-5_9
DO - 10.1007/978-3-319-70848-5_9
M3 - Conference contribution
T3 - Formal Methods: Foundations and Applications
SP - 125
EP - 141
BT - Brazilian Symposium on Formal Methods
ER -