OptCE: A Counterexample-Guided Inductive Optimization Solver

Higo F. Albuquerque, Rodrigo F. Araújo, Iury V. Bessa, Lucas C. Cordeiro, Eddie B. De Lima Filho

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

152 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationBrazilian Symposium on Formal Methods
Number of pages16
Publication statusPublished - 2017

Publication series

NameFormal Methods: Foundations and Applications
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'OptCE: A Counterexample-Guided Inductive Optimization Solver'. Together they form a unique fingerprint.

Cite this