{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:18:47Z","timestamp":1740028727217,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_38","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"521-536","source":"Crossref","is-referenced-by-count":16,"title":["An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic"],"prefix":"10.1007","author":[{"given":"Sergey","family":"Berezin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. A Framework for Cooperating Decision Procedures. In David McAllester, editor, 17th International Conference on Computer Aided Deduction, volume 1831 of LNAI, pages 79\u201397. Springer-Verlag, 2000.","DOI":"10.1007\/10721959_6"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. A Generalization of Shostak\u2019s Method for Combining Decision Procedures. In 4th International Workshop on Frontiers of Combining Systems (FroCos), 2002.","DOI":"10.1007\/3-540-45988-X_11"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In 14th International Conference on Computer-Aided Verification, 2002.","DOI":"10.1007\/3-540-45657-0_18"},{"key":"38_CR4","doi-asserted-by":"crossref","unstructured":"Sergey Berezin, Vijay Ganesh, and David L. Dill. Online proof-producing decision procedure for mixed-integer linear arithmetic. Unpublished manuscript. URL: http:\/\/www.cs.cmu.edu\/~berez\/publications.html , 2002.","DOI":"10.1007\/3-540-36577-X_38"},{"key":"38_CR5","volume-title":"Introduction to Linear Optimization","author":"D. Bertsimas","year":"1997","unstructured":"Dimitris Bertsimas and John N. Tsitsiklis. Introduction to Linear Optimization. Athena Scientific, Belmont, Massachusetts, 1997."},{"key":"38_CR6","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"G. B. Dantzig","year":"1973","unstructured":"George B. Dantzig and B. Curtis Eaves. Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A), 14:288\u2013297, 1973.","journal-title":"Journal of Combinatorial Theory (A)"},{"issue":"3","key":"38_CR7","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201\u2013215, July 1960. au[GMP]_GMP library for arbitrary precision arithmetic. URL: http:\/\/swox.com\/gmp .","journal-title":"Journal of the ACM"},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhaod, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In 39th Design Automation Conference, 2001.","DOI":"10.1145\/378239.379017"},{"key":"38_CR9","doi-asserted-by":"crossref","unstructured":"M. Oliver M\u00f6ller. Solving bit-vector equations-a decision procedure for hardware verification, 1998. Diploma Thesis, available at http:\/\/www.informatik.uni-ulm.de\/ki\/Bitvector\/ .","DOI":"10.1007\/3-540-49519-3_4"},{"issue":"5","key":"38_CR10","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Marques-Silva","year":"1999","unstructured":"J. Marques-Silva and K. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers, 48(5):506\u2013521, 1999.","journal-title":"IEEE Transactions on Computers"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. Proof generation in the Touchstone theorem prover. In David McAllester, editor, 17th International Conference on Computer-Aided Deduction, volume 1831 of Lecture Notes in Artificial Intelligence. Springer-Verlag, June 2000. Pittsburgh, Pennsylvania.","DOI":"10.1007\/10721959_3"},{"issue":"2","key":"38_CR12","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u201357, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"38_CR13","doi-asserted-by":"crossref","unstructured":"William Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. In Supercomputing, pages 4\u201313, 1991.","DOI":"10.1145\/125826.125848"},{"key":"38_CR14","doi-asserted-by":"crossref","unstructured":"H. Ruess and N. Shankar. Deconstructing Shostak. In 16th IEEE Symposium on Logic in Computer Science, 2001.","DOI":"10.1109\/LICS.2001.932479"},{"key":"38_CR15","doi-asserted-by":"crossref","unstructured":"A. Stump, C. Barrett, and D. Dill. CVC: a Cooperating Validity Checker. In 14th International Conference on Computer-Aided Verification, 2002.","DOI":"10.1007\/3-540-45657-0_40"},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"A. Stump, C. Barrett, D. Dill, and J. Levitt.ADecision Procedure for an Extensional Theory of Arrays. In 16th IEEE Symposium on Logic in Computer Science, pages 29\u201337. IEEE Computer Society, 2001.","DOI":"10.1109\/LICS.2001.932480"},{"issue":"1","key":"38_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. Shostak","year":"1984","unstructured":"R. Shostak. Deciding combinations of theories. Journal of the Association for Computing Machinery, 31(1):1\u201312, 1984.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"38_CR18","doi-asserted-by":"crossref","unstructured":"J. P. M. Silva and K.A. Sakallah. GRASP-Anewsearch algorithm for satisfiability. In Proceedings of the ACM\/IEEE International Conference on Computer-Aided Design, pages 220\u2013227, 11 1996.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"38_CR19","unstructured":"A. Stump. Checking Validities and Proofs with CVC and flea. PhD thesis, Stanford University, 2002. In preparation: check http:\/\/verify.stanford.edu\/~stump\/ for a draft."},{"key":"38_CR20","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/0097-3165(76)90055-8","volume":"21","author":"H. P. Williams","year":"1976","unstructured":"H. P. Williams. Fourier-Motzkin elimination extension to integer programming problems. Journal of Combinatorial Theory (A), 21:118\u2013123, 1976.","journal-title":"Journal of Combinatorial Theory (A)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:11:50Z","timestamp":1739992310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_38","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}