{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:14:59Z","timestamp":1770894899062,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319409696","type":"print"},{"value":"9783319409702","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_18","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"284-301","source":"Crossref","is-referenced-by-count":2,"title":["Speeding up the Constraint-Based Method in Difference Logic"],"prefix":"10.1007","author":[{"given":"Lorenzo","family":"Candeago","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Larraz","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[]},{"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","first-page":"682","volume-title":"Verification: Theory and Practice","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Petri net analysis using invariant generation. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 682\u2013701. Springer, Heidelberg (2004)"},{"issue":"1","key":"18_CR3","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25\u201355 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/978-3-642-35873-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Larraz","year":"2013","unstructured":"Larraz, D., Rodr\u00edguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169\u2013188. Springer, Heidelberg (2013)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: Proceeding FMCAD 2013, pp. 218\u2013225. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"779","DOI":"10.1007\/978-3-319-08867-9_52","volume-title":"Computer Aided Verification","author":"D Larraz","year":"2014","unstructured":"Larraz, D., Nimkar, K., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779\u2013796. Springer, Heidelberg (2014)"},{"issue":"1","key":"18_CR9","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/s10817-010-9196-8","volume":"48","author":"C Borralleras","year":"2012","unstructured":"Borralleras, C., Lucas, S., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: SAT modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning 48(1), 107\u2013131 (2012)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/978-3-319-09284-3_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"D Larraz","year":"2014","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 333\u2013350. Springer, Heidelberg (2014)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation : a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proceeding POPL 1977, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceeding POPL 1978, pp. 84\u201396. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceeding 2nd International Symposium on Programming, pp. 106\u2013130 (1976)","DOI":"10.1145\/390018.808314"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"issue":"1","key":"18_CR16","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symbolic Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symbolic Comput."},{"key":"18_CR17","unstructured":"Menasche, M., Berthomieu, B.: Time petri nets for analyzing and verifying time dependent communication protocols. In: Protocol Specification, Testing, and Verification, pp. 161\u2013172 (1983)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","first-page":"197","volume-title":"Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1989","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1989)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Model checking timed automata. In: Lectures on Embedded Systems, European Educational Forum, School on Embedded Systems. vol. 1494. LNCS, pp. 114\u2013152. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-65193-4_20"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Compositional safety verification with Max-SMT. In: Proceeding FMCAD 2015, pp. 33\u201340. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542250"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-642-36675-8_11","volume-title":"Automated Reasoning and Mathematics","author":"D Kapur","year":"2013","unstructured":"Kapur, D., Zhang, Z., Horbach, M., Zhao, H., Lu, Q., Nguyen, T.V.: Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariants. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 189\u2013228. Springer, Heidelberg (2013)"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Automatic modular abstractions for linear constraints. In: Proceeding POPL 2009, pp. 140\u2013151. ACM (2009)","DOI":"10.1145\/1594834.1480899"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/11559306_9","volume-title":"Frontiers of Combining Systems","author":"SK Lahiri","year":"2005","unstructured":"Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 168\u2013183. Springer, Heidelberg (2005)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-540-89439-1_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Monniaux","year":"2008","unstructured":"Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243\u2013257. Springer, Heidelberg (2008)"},{"key":"18_CR25","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1998","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Amsterdam (1998)"},{"issue":"1\u20133","key":"18_CR26","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0004-3702(91)90006-6","volume":"49","author":"R Dechter","year":"1991","unstructured":"Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artif. Intell. 49(1\u20133), 61\u201395 (1991)","journal-title":"Artif. Intell."},{"key":"18_CR27","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2001","unstructured":"Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms, 2nd edn. McGraw-Hill Higher Education, New York (2001)","edition":"2"},{"issue":"1\u20133","key":"18_CR28","first-page":"143","volume":"35","author":"AM Frisch","year":"2005","unstructured":"Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.W.: Solving non-boolean satisfiability problems with stochastic local search: a comparison of encodings. J. Autom. Reasoning 35(1\u20133), 143\u2013179 (2005)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11499107_1","volume-title":"Theory and Applications of Satisfiability Testing","author":"J Argelich","year":"2005","unstructured":"Argelich, J., Many\u00e0, F.: Solving over-constrained problems with SAT technology. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 1\u201315. Springer, Heidelberg (2005)"},{"key":"18_CR30","volume-title":"Numerical Recipes: The Art of Scientific Computing","author":"WH Press","year":"1989","unstructured":"Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes: The Art of Scientific Computing. Cambridge Univ. Press, NewYork (1989)"},{"issue":"3\u20134","key":"18_CR31","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/s10472-011-9233-2","volume":"62","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Argelich, J., Gra\u00e7a, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3\u20134), 317\u2013343 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2015)"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.: $${\\nu }z$$ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015)"},{"key":"18_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The Barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294\u2013298. Springer, Heidelberg (2008)"},{"key":"18_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T12:13:30Z","timestamp":1656677610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}