{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:02:27Z","timestamp":1743058947709,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319662626"},{"type":"electronic","value":"9783319662633"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_24","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T04:05:11Z","timestamp":1502165111000},"page":"380-397","source":"Crossref","is-referenced-by-count":2,"title":["A Benders Decomposition Approach to Deciding Modular Linear Integer Arithmetic"],"prefix":"10.1007","author":[{"given":"Bishoksan","family":"Kafle","sequence":"first","affiliation":[]},{"given":"Graeme","family":"Gange","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schachte","sequence":"additional","affiliation":[]},{"given":"Harald","family":"S\u00f8ndergaard","sequence":"additional","affiliation":[]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-12002-2_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bardin","year":"2010","unstructured":"Bardin, S., Herrmann, P., Perroud, F.: An alternative to SAT-based approaches for bit-vectors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 84\u201398. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-12002-2_7"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22110-1_14"},{"key":"24_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). \nwww.SMT-LIB.org"},{"issue":"1","key":"24_CR4","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/BF01386316","volume":"4","author":"JF Benders","year":"1962","unstructured":"Benders, J.F.: Partitioning procedures for solving mixed-variables programming problems. Numer. Math. 4(1), 238\u2013252 (1962)","journal-title":"Numer. Math."},{"key":"24_CR5","unstructured":"Bj\u00f8rner, N., Blass, A., Gurevich, Y., Musuvathi, M.: Modular difference logic is hard, November 2008, Unpublished. \narXiv:0811.0987v1"},{"issue":"2","key":"24_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2005.12.001","volume":"144","author":"M Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Hanna, Z., Khasidashvili, Z., Palti, A., Sebastiani, R.: Encoding RTL constructs for MathSAT: a preliminary report. Electron. Notes Theor. Comput. Sci. 144(2), 3\u201314 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proceedings of the ASPDAC\/VLSI Design Conference 2002, pp. 741\u2013746. IEEE Computer Society Press (2002)","DOI":"10.1109\/ASPDAC.2002.995022"},{"key":"24_CR8","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). doi:\n10.1007\/978-3-642-00768-2_16"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-540-73368-3_54","volume-title":"Computer Aided Verification","author":"R Bruttomesso","year":"2007","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A lazy and layered SMT(\n            $$\\cal{BV}$$\n          ) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 547\u2013560. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-73368-3_54"},{"key":"24_CR10","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). doi:\n10.1007\/978-3-642-36742-7_7"},{"key":"24_CR11","unstructured":"Conchon, S., D\u00e9harbe, D., Heizmann, M., Weber, T.: SMT-COMP (2016). \nhttp:\/\/smtcomp.sourceforge.net\/2016\/"},{"key":"24_CR12","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2009)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). doi:\n10.1007\/978-3-540-31987-0_3"},{"key":"24_CR14","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 Moura de","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). doi:\n10.1007\/978-3-540-78800-3_24"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 15\u201344. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-36675-8_2"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_49"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Ferrandi, F., Rendine, M., Sciuto, D.: Functional verification for SystemC descriptions using constraint solving. In: 2002 Design, Automation and Test in Europe Conference and Exposition (DATE 2002), pp. 744\u2013751. IEEE Computer Society Press (2002)","DOI":"10.1109\/DATE.2002.998382"},{"key":"24_CR18","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: Efficiently solving bit-vector problems using model checkers. In: SMT Workshop (2013)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-38536-0_33","volume-title":"Computer Science \u2013 Theory and Applications","author":"A Fr\u00f6hlich","year":"2013","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 378\u2013390. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-38536-0_33"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-73368-3_52"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-38574-2_15","volume-title":"Automated Deduction \u2013 CADE-24","author":"G Gange","year":"2013","unstructured":"Gange, G., S\u00f8ndergaard, H., Stuckey, P.J., Schachte, P.: Solving difference constraints over modular arithmetic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 215\u2013230. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-38574-2_15"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21690-4_20"},{"key":"24_CR23","unstructured":"Gurobi Optimization, Inc.: Gurobi optimizer reference manual (2016). \nhttp:\/\/www.gurobi.com"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1007\/978-3-319-08867-9_45","volume-title":"Computer Aided Verification","author":"L Hadarean","year":"2014","unstructured":"Hadarean, L., Bansal, K., Jovanovi\u0107, D., Barrett, C., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 680\u2013695. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_45"},{"issue":"1","key":"24_CR25","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10107-003-0375-9","volume":"96","author":"JN Hooker","year":"2003","unstructured":"Hooker, J.N., Ottosson, G.: Logic-based Benders decomposition. Math. Program. 96(1), 33\u201360 (2003)","journal-title":"Math. Program."},{"key":"24_CR26","volume-title":"Software Abstractions: Logic, Language and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02658-4_52"},{"key":"24_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-662-44465-8_41","volume-title":"Mathematical Foundations of Computer Science 2014","author":"G Kov\u00e1sznai","year":"2014","unstructured":"Kov\u00e1sznai, G., Veith, H., Fr\u00f6hlich, A., Biere, A.: On the complexity of symbolic verification and decision problems in bit-vector logic. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014. LNCS, vol. 8635, pp. 481\u2013492. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-662-44465-8_41"},{"key":"24_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-33558-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"LD Michel","year":"2012","unstructured":"Michel, L.D., Hentenryck, P.V.: Constraint satisfaction over bit-vectors. In: Milano, M. (ed.) CP 2012. LNCS, pp. 527\u2013543. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-33558-7_39"},{"issue":"2","key":"24_CR30","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10107-003-0433-3","volume":"99","author":"A Neumaier","year":"2004","unstructured":"Neumaier, A., Shcherbina, O.: Safe bounds in linear and mixed-integer linear programming. Math. Program. 99(2), 283\u2013296 (2004)","journal-title":"Math. Program."},{"issue":"2","key":"24_CR31","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/s10107-005-0585-4","volume":"103","author":"A Neumaier","year":"2005","unstructured":"Neumaier, A., Shcherbina, O., Huyer, W., Vink\u00f3, T.: A comparison of complete global optimization solvers. Math. Program. 103(2), 335\u2013356 (2005)","journal-title":"Math. Program."},{"key":"24_CR32","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. J. Satisf. Boolean Model. Comput. 9, 53\u201358 (2014). (published 2015)"},{"key":"24_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-319-10428-7_42","volume-title":"Principles and Practice of Constraint Programming","author":"R Nieuwenhuis","year":"2014","unstructured":"Nieuwenhuis, R.: The IntSat method for integer linear programming. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 574\u2013589. Springer, Cham (2014). doi:\n10.1007\/978-3-319-10428-7_42"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Parthasarathy, G., Iyer, M.K., Cheng, K., Wang, L.: An efficient finite-domain constraint solver for circuits. In: Malik, S., Fix, L., Kahng, A.B. (eds.) Proceedings of the 41th Design Automation Conference (DAC 2004), pp. 212\u2013217. ACM Publ. (2004)","DOI":"10.1145\/996566.996628"},{"issue":"2","key":"24_CR35","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1109\/92.386221","volume":"3","author":"R Vemuri","year":"1995","unstructured":"Vemuri, R., Kalyanaraman, R.: Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming. IEEE Trans. VLSI Syst. 3(2), 201\u2013214 (1995)","journal-title":"IEEE Trans. VLSI Syst."},{"key":"24_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-319-33954-2_27","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"W Wang","year":"2016","unstructured":"Wang, W., S\u00f8ndergaard, H., Stuckey, P.J.: A bit-vector solver with word-level propagation. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 374\u2013391. Springer, Cham (2016). doi:\n10.1007\/978-3-319-33954-2_27"},{"key":"24_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-40970-2_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"A Zelji\u0107","year":"2016","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 249\u2013266. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40970-2_16"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T14:50:46Z","timestamp":1502203846000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}