{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:28:59Z","timestamp":1693610939517},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,9,30]],"date-time":"2011-09-30T00:00:00Z","timestamp":1317340800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2011,12]]},"DOI":"10.1007\/s10703-011-0127-z","type":"journal-article","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T11:46:15Z","timestamp":1317296775000},"page":"246-260","source":"Crossref","is-referenced-by-count":5,"title":["Cuts from proofs: a complete and practical technique for solving linear inequalities over integers"],"prefix":"10.1007","volume":"39","author":[{"given":"Isil","family":"Dillig","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Dillig","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,9,30]]},"reference":[{"key":"127_CR1","doi-asserted-by":"crossref","DOI":"10.1145\/512760.512770","volume-title":"Automatic discovery of linear restraints among variables of a program","author":"P Cousot","year":"1978","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. ACM, New York, pp\u00a084\u201397"},{"key":"127_CR2","doi-asserted-by":"crossref","unstructured":"Pugh W (1992) The Omega test: a fast and practical integer programming algorithm for dependence analysis. Commun ACM","DOI":"10.1145\/125826.125848"},{"key":"127_CR3","first-page":"741","volume-title":"VLSI design","author":"R Brinkmann","year":"2002","unstructured":"Brinkmann R, Drechsler R (2002) RTL-datapath verification using integer linear programming. In: VLSI design, pp\u00a0741\u2013746"},{"key":"127_CR4","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1145\/266021.266071","volume-title":"DAC \u201997: Proceedings of the 34th annual conference on design automation","author":"T Amon","year":"1997","unstructured":"Amon T, Borriello G, Hu T, Liu J (1997) Symbolic timing verification of timing diagrams using Presburger formulas. In: DAC \u201997: Proceedings of the 34th annual conference on design automation. ACM, New York, pp 226\u2013231"},{"key":"127_CR5","unstructured":"Dutertre B, De Moura L (2006) The Yices SMT solver. Technical report, SRI International"},{"key":"127_CR6","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. Tools and algorithms for the construction and analysis of systems, April 2008, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"127_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Proceedings of the 19th international conference on computer aided verification","author":"C Barrett","year":"2007","unstructured":"Barrett C, Tinelli C (2007) CVC3. In: Damm W, Hermanns H (eds) Proceedings of the 19th international conference on computer aided verification. Lecture notes in computer science, vol 4590. Springer, Berlin, pp 298\u2013302"},{"key":"127_CR8","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Proceedings of the 20th international conference on computer aided verification","author":"R Bruttomesso","year":"2008","unstructured":"Bruttomesso R, Cimatti A, Franz\u00e9n A, Griggio A, Sebastiani R (2008) The MathSAT4 SMT solver. In: Proceedings of the 20th international conference on computer aided verification. Springer, Berlin\/Heidelberg, pp 299\u2013303"},{"key":"127_CR9","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Proceedings of the 20th international conference on computer aided verification","author":"M Bofill","year":"2008","unstructured":"Bofill M, Nieuwenhuis R, Oliveras A, Rodr\u00edguez-Carbonell E, Rubio A (2008) The Barcelogic smt solver. In: Proceedings of the 20th international conference on computer aided verification. Springer, Berlin\/Heidelberg, pp 294\u2013298"},{"key":"127_CR10","volume-title":"Linear programming and extensions","author":"G Dantzig","year":"1963","unstructured":"Dantzig G (1963) Linear programming and extensions. Princeton University Press, Princeton"},{"key":"127_CR11","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/3-540-36126-X_11","volume-title":"FMCAD \u201902: Proceedings of the 4th international conference on formal methods in computer-aided design","author":"V Ganesh","year":"2002","unstructured":"Ganesh V, Berezin S, Dill D (2002) Deciding Presburger arithmetic by model checking and comparisons with other methods. In: FMCAD \u201902: Proceedings of the 4th international conference on formal methods in computer-aided design. Springer, London, pp 171\u2013186"},{"key":"127_CR12","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A (1986) Theory of linear and integer programming. Wiley, New York"},{"key":"127_CR13","doi-asserted-by":"crossref","DOI":"10.1002\/9781118627372","volume-title":"Integer and combinatorial optimization","author":"GL Nemhauser","year":"1988","unstructured":"Nemhauser GL, Wolsey L (1988) Integer and combinatorial optimization. Wiley, New York"},{"key":"127_CR14","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1145\/236869.237083","volume-title":"Proc int\u2019l symp on symbolic and algebraic computation: ISSAC \u201996","author":"A Storjohann","year":"1996","unstructured":"Storjohann A, Labahn G (1996) Asymptotically fast computation of Hermite normal forms of integer matrices. In: Proc int\u2019l symp on symbolic and algebraic computation: ISSAC \u201996. ACM Press, New York, pp 259\u2013266"},{"key":"127_CR15","unstructured":"http:\/\/gmplib.org\/ : Gnu mp bignum library"},{"key":"127_CR16","series-title":"Graduate texts in mathematics","doi-asserted-by":"crossref","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 (1993) A course in computational algebraic number theory. Graduate texts in mathematics. Springer, Berlin"},{"issue":"1","key":"127_CR17","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1287\/moor.12.1.50","volume":"12","author":"P Domich","year":"1987","unstructured":"Domich P, Kannan R, Trotter L (1987) J.: Hermite normal form computation using modulo determinant arithmetic. Mathematics of Operations Research 12(1):50\u201359","journal-title":"Mathematics of Operations Research"},{"key":"127_CR18","unstructured":"http:\/\/www.smtcomp.org : Smt-comp\u201908"},{"key":"127_CR19","unstructured":"http:\/\/www.gnu.org\/software\/glpk\/ : Glpk (gnu linear programming kit)"},{"key":"127_CR20","unstructured":"http:\/\/lpsolve.sourceforge.net\/5.5\/ : lp_solve reference guide"},{"key":"127_CR21","unstructured":"http:\/\/www.ilog.com\/products\/cplex\/ : Cplex"},{"key":"127_CR22","doi-asserted-by":"crossref","unstructured":"Seshia S, Bryant R (2004) Deciding quantifier-free Presburger formulas using parameterized solution bounds","DOI":"10.21236\/ADA461078"},{"key":"127_CR23","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/978-3-540-70545-1_24","volume-title":"Proceedings of the 20th international conference on computer aided verification","author":"H Jain","year":"2008","unstructured":"Jain H, Clarke E, Grumberg O (2008) Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. In: Proceedings of the 20th international conference on computer aided verification. Springer, Berlin\/Heidelberg, pp 254\u2013267"},{"key":"127_CR24","first-page":"21","volume-title":"Proceedings of the symposium on static analysis (SAS)","author":"P Wolper","year":"1995","unstructured":"Wolper P, Boigelot B (1995) An automata-theoretic approach to Presburger arithmetic constraints. In: Proceedings of the symposium on static analysis (SAS), pp\u00a021\u201332"},{"key":"127_CR25","doi-asserted-by":"crossref","unstructured":"Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symb Log 269\u2013285","DOI":"10.2307\/2963594"},{"key":"127_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Proceedings of tools and algorithms for the construction and analysis of systems (TACAS)","author":"KL McMillan","year":"2005","unstructured":"McMillan KL (2005) Applications of Craig interpolants in model checking. In: Proceedings of tools and algorithms for the construction and analysis of systems (TACAS), pp\u00a01\u201312"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0127-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0127-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0127-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T15:00:30Z","timestamp":1560697230000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0127-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,30]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["127"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0127-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9,30]]}}}