{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:00:45Z","timestamp":1760061645995,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026577"},{"type":"electronic","value":"9783642026584"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02658-4_20","type":"book-chapter","created":{"date-parts":[[2009,6,22]],"date-time":"2009-06-22T11:00:16Z","timestamp":1245668416000},"page":"233-247","source":"Crossref","is-referenced-by-count":38,"title":["Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers"],"prefix":"10.1007","author":[{"given":"Isil","family":"Dillig","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Dillig","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","first-page":"84","volume-title":"Automatic discovery of linear restraints among variables of a program","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM (1992)","DOI":"10.1145\/135226.135233"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: VLSI Design, pp. 741\u2013746 (2002)","DOI":"10.1109\/ASPDAC.2002.995022"},{"key":"20_CR4","first-page":"226","volume-title":"DAC 1997: Proceedings of the 34th annual conference on Design automation","author":"T. Amon","year":"1997","unstructured":"Amon, T., Borriello, G., Hu, T., Liu, J.: Symbolic timing verification of timing diagrams using presburger formulas. In: DAC 1997: Proceedings of the 34th annual conference on Design automation, pp. 226\u2013231. ACM, New York (1997)"},{"key":"20_CR5","unstructured":"Dutertre, B., De Moura, L.: The yices SMT solver. Technical report, SRI International (2006)"},{"key":"20_CR6","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The mathsat 4 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a05123, pp. 294\u2013298. Springer, Heidelberg (2008)"},{"key":"20_CR10","doi-asserted-by":"publisher","DOI":"10.1515\/9781400884179","volume-title":"Linear Programming and Extensions","author":"G. Dantzig","year":"1963","unstructured":"Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/3-540-36126-X_11","volume-title":"Formal Methods in Computer-Aided Design","author":"V. Ganesh","year":"2002","unstructured":"Ganesh, V., Berezin, S., Dill, D.: Deciding presburger arithmetic by model checking and comparisons with other methods. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 171\u2013186. Springer, Heidelberg (2002)"},{"key":"20_CR12","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. J. Wiley & Sons, Chichester (1986)"},{"key":"20_CR13","doi-asserted-by":"publisher","DOI":"10.1002\/9781118627372","volume-title":"Integer and Combinatorial Optimization","author":"G.L. Nemhauser","year":"1988","unstructured":"Nemhauser, G.L., Wolsey, L.: Integer and Combinatorial Optimization. John Wiley & Sons, Chichester (1988)"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/236869.237083","volume-title":"Proc. Int\u2019l. Symp. on Symbolic and Algebraic Computation: ISSAC 1996","author":"A. Storjohann","year":"1996","unstructured":"Storjohann, A., Labahn, G.: Asymptotically fast computation of hermite normal forms of integer matrices. In: Proc. Int\u2019l. Symp. on Symbolic and Algebraic Computation: ISSAC 1996, pp. 259\u2013266. ACM Press, New York (1996)"},{"key":"20_CR15","unstructured":"http:\/\/gmplib.org\/: Gnu mp bignum library"},{"key":"20_CR16","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02945-9","volume-title":"A Course in Computational Algebraic Number Theory","author":"H. Cohen","year":"1993","unstructured":"Cohen, H.: A Course in Computational Algebraic Number Theory. Graduate Texts in Mathematics. Springer, Heidelberg (1993)"},{"issue":"1","key":"20_CR17","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1287\/moor.12.1.50","volume":"12","author":"P. Domich","year":"1987","unstructured":"Domich, P., Kannan, R., Trotter, J.L.: Hermite normal form computation using modulo determinant arithmetic. Mathematics of Operations Research\u00a012(1), 50\u201359 (1987)","journal-title":"Mathematics of Operations Research"},{"key":"20_CR18","unstructured":"http:\/\/www.smtcomp.org : Smt-comp 2008"},{"key":"20_CR19","unstructured":"http:\/\/www.gnu.org\/software\/glpk\/: Glpk (gnu linear programming kit)"},{"key":"20_CR20","unstructured":"http:\/\/lpsolve.sourceforge.net\/5.5\/: lp_solve reference guide"},{"key":"20_CR21","unstructured":"http:\/\/www.ilog.com\/products\/cplex\/: Cplex"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-540-70545-1_24","volume-title":"Computer Aided Verification","author":"H. Jain","year":"2008","unstructured":"Jain, H., Clarke, E., Grumberg, O.: Efficient craig interpolation for linear diophantine (dis)equations and linear modular equations. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 254\u2013267. Springer, Heidelberg (2008)"},{"key":"20_CR23","unstructured":"Golub, G.H., Van Loan, C.F.: Matrix Computations. JHU Press (1996)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02658-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T07:58:15Z","timestamp":1739174295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02658-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026577","9783642026584"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02658-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}