{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:22:44Z","timestamp":1743031364332,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319708478"},{"type":"electronic","value":"9783319708485"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70848-5_9","type":"book-chapter","created":{"date-parts":[[2017,11,10]],"date-time":"2017-11-10T10:43:26Z","timestamp":1510310606000},"page":"125-141","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["OptCE: A Counterexample-Guided Inductive Optimization Solver"],"prefix":"10.1007","author":[{"given":"Higo F.","family":"Albuquerque","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rodrigo F.","family":"Ara\u00fajo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iury V.","family":"Bessa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eddie B.","family":"de Lima Filho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,11]]},"reference":[{"issue":"12","key":"9_CR1","doi-asserted-by":"crossref","first-page":"6201","DOI":"10.1021\/acs.jctc.6b00819","volume":"12","author":"H Park","year":"2016","unstructured":"Park, H., Bradley, P., Greisen Jr., P., Liu, Y., Mulligan, V.K., Kim, D.E., Baker, D., DiMaio, F.: Simultaneous optimization of biomolecular energy functions on features from small molecules and macromolecules. J. Chem. Theory Comput. 12(12), 6201\u20136212 (2016)","journal-title":"J. Chem. Theory Comput."},{"key":"9_CR2","volume-title":"Engineering a Compiler","author":"KD Cooper","year":"2004","unstructured":"Cooper, K.D., Torczon, L.: Engineering a Compiler. Morgan Kaufmann, San Francisco (2004)"},{"key":"9_CR3","volume-title":"Optimization for Engineering Design: Algorithms and Examples","author":"K Deb","year":"2004","unstructured":"Deb, K.: Optimization for Engineering Design: Algorithms and Examples. Prentice-Hall of India, New Delhi (2004)"},{"issue":"1","key":"9_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/TSMCC.2007.905812","volume":"38","author":"K Vergidis","year":"2008","unstructured":"Vergidis, K., Tiwari, A., Majeed, B.: Business process analysis and optimization: beyond reengineering. IEEE Trans. Syst. Man Cybern. C Appl. Rev. 38(1), 69\u201382 (2008)","journal-title":"IEEE Trans. Syst. Man Cybern. C Appl. Rev."},{"volume-title":"Simulated Annealing: Theory and Applications","year":"1987","key":"9_CR5","unstructured":"Laarhoven, P.J.M., Aarts, E.H.L. (eds.): Simulated Annealing: Theory and Applications. Kluwer Academic Publishers, Norwell (1987)"},{"key":"9_CR6","volume-title":"Particle Swarm Optimization: Theory, Techniques and Applications, Engineering tools, Techniques and Tables","author":"A Olsson","year":"2011","unstructured":"Olsson, A.: Particle Swarm Optimization: Theory, Techniques and Applications, Engineering tools, Techniques and Tables. Nova Science Publishers, USA (2011)"},{"key":"9_CR7","volume-title":"Genetic Algorithms in Search, Optimization, and Machine Learning, Artificial Intelligence","author":"D Goldberg","year":"1989","unstructured":"Goldberg, D.: Genetic Algorithms in Search, Optimization, and Machine Learning, Artificial Intelligence. Addison-Wesley Publishing Company, Boston (1989)"},{"key":"9_CR8","series-title":"Nonconvex Optimization and Its Applications","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4949-6","volume-title":"Deterministic Global Optimization","author":"C Floudas","year":"2000","unstructured":"Floudas, C.: Deterministic Global Optimization. Nonconvex Optimization and Its Applications. Springer, Berlin (2000). https:\/\/doi.org\/10.1007\/978-1-4757-4949-6"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Ara\u00fajo, R., Bessa, I., Cordeiro, L., Filho, J.E.C.: SMT-based verification applied to non-convex optimization problems. In: SBESC, pp. 1\u20138 (2016)","DOI":"10.1109\/SBESC.2016.010"},{"key":"9_CR10","unstructured":"Ara\u00fajo, R., Bessa, I., Cordeiro, L., Filho, J.E.C.: Counterexample guided inductive optimization, pp. 1\u201332 (2017). arXiv:1704.03738 [cs.AI]"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Alur, R., Bodik, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD, pp. 1\u20138 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-10672-9_3","volume-title":"Programming Languages and Systems","author":"A Solar-Lezama","year":"2009","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4\u201313. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_3"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"issue":"4","key":"9_CR14","first-page":"957","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE TSE 38(4), 957\u2013974 (2012)","journal-title":"IEEE TSE"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"9_CR19","unstructured":"Jamil, M., Yang, X.: A literature survey of benchmark functions for global optimization problems, CoRR abs\/1308.4008. http:\/\/arxiv.org\/abs\/1308.4008"},{"key":"9_CR20","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-54862-8_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Morse","year":"2014","unstructured":"Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 405\u2013407. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_31"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Hutter, F., Babic, D., Hoos, H.H., Hu, A.J.: Boosting verification by automatic tuning of decision procedures. In: FMCAD, pp. 27\u201334 (2007)","DOI":"10.1109\/FAMCAD.2007.9"},{"key":"9_CR23","unstructured":"The Mathworks Inc, Matlab Optimization Toolbox User\u2019s Guide (2016)"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156\u2013169. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_18"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pister, M., Tautschnig, M.: Tool-support for the analysis of hybrid systems and models. In: DATE, pp. 924\u2013929 (2007)","DOI":"10.1109\/DATE.2007.364411"},{"key":"9_CR26","unstructured":"Nuzzo, P., Puggelli, A.A.A., Seshia, S.A., Sangiovanni-Vincentelli, A.L.: CalCS: SMT solving for non-linear convex constraints, Technical report UCB\/EECS-2010-100, EECS Department, University of California, Berkeley, Jun 2010"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Shoukry, Y., Nuzzo, P., Saha, I., Sangiovanni-Vincentelli, A.L., Seshia, S.A., Pappas, G.J., Tabuada, P.: Scalable lazy smt-based motion planning. In: CDC, pp. 6683\u20136688 (2016)","DOI":"10.1109\/CDC.2016.7799298"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Shoukry, Y., Nuzzo, P., Sangiovanni-Vincentelli, A.L., Seshia, S.A., Pappas, G.J., Tabuada, P.: SMC: satisfiability modulo convex optimization. In: HSCC, pp. 19\u201328 (2017)","DOI":"10.1145\/3049797.3049819"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: VZ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT Solvers. In: POPL, pp. 607\u2013618 (2014)","DOI":"10.1145\/2535838.2535857"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-21690-4_27","volume-title":"Computer Aided Verification","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 447\u2013454. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_27"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Trindade, A., Ismail, H., Cordeiro, L.: Applying multi-core model checking to hardware-software partitioning in embedded systems. In: SBESC, pp. 102\u2013105 (2015)","DOI":"10.1109\/SBESC.2015.26"},{"issue":"1","key":"9_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10617-015-9163-z","volume":"20","author":"A Trindade","year":"2016","unstructured":"Trindade, A., Cordeiro, L.: Applying SMT-based verification to hardware\/software partitioning in embedded systems. Des. Autom. Embed. Syst. 20(1), 1\u201319 (2016)","journal-title":"Des. Autom. Embed. Syst."},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Rocha, H., Ismail, H., Cordeiro, L., Barreto, R.: Model checking embedded C software using k-induction and invariants. In: SBESC, pp. 90\u201395 (2015)","DOI":"10.1109\/SBESC.2015.24"},{"issue":"1","key":"9_CR35","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10009-015-0407-9","volume":"19","author":"MYR Gadelha","year":"2017","unstructured":"Gadelha, M.Y.R., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. STTT 19(1), 97\u2013114 (2017)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70848-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:36:57Z","timestamp":1570307817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70848-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319708478","9783319708485"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70848-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}