{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:11:09Z","timestamp":1748664669949,"version":"3.41.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319251493"},{"type":"electronic","value":"9783319251509"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-25150-9_20","type":"book-chapter","created":{"date-parts":[[2015,9,25]],"date-time":"2015-09-25T11:42:36Z","timestamp":1443181356000},"page":"328-345","source":"Crossref","is-referenced-by-count":2,"title":["A Graphical Theorem of the Alternative for UTVPI Constraints"],"prefix":"10.1007","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0055766","volume-title":"Mathematical Foundations of Computer Science 1998","author":"M Alekhnovich","year":"1998","unstructured":"Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol. 1450, p. 176. Springer, Heidelberg (1998)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-540-78163-9_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: An improved tight closure algorithm for integer octagonal constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 8\u201321. Springer, Heidelberg (2008)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"20_CR4","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.disopt.2012.11.001","volume":"10","author":"R Chandrasekaran","year":"2013","unstructured":"Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for horn programs. Discrete Optimization 10, 85\u2013101 (2013)","journal-title":"Discrete Optimization"},{"key":"20_CR6","unstructured":"Duterre, B., de Moura, L.: The yices smt solver. Technical report, SRI International (2006)"},{"issue":"3","key":"20_CR7","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1109\/12.372041","volume":"44","author":"R Gerber","year":"1995","unstructured":"Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Comput. 44(3), 471\u2013479 (1995)","journal-title":"IEEE Trans. Comput."},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","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":"20_CR9","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Proceedings of the Eighth Working Conference on Reverse Engineering, pp. 310\u2013319 (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"issue":"1","key":"20_CR10","doi-asserted-by":"publisher","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. Ord. Symbolic Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Ord. Symbolic Comput."},{"key":"20_CR11","volume-title":"The LEDA Platform of Combinatorial and Geometric Computing","author":"K Mehlhorn","year":"1999","unstructured":"Mehlhorn, K., N\u00e4her, S.: The LEDA Platform of Combinatorial and Geometric Computing. Cambridge University Press, Cambridge (1999)"},{"key":"20_CR12","unstructured":"Revesz, P.Z.: Tightened transitive closure of integer addition constraints. In: SARA (2009)"},{"key":"20_CR13","unstructured":"Rubinfield, R.: A Mathematical Theory of Self-checking, Self-testing and self-correcting Programs. Ph.D. thesis, Computer Science Division, University of California, Berkeley (1990)"},{"key":"20_CR14","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1987","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1987)"},{"issue":"4","key":"20_CR15","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1287\/ijoc.1090.0369","volume":"22","author":"A Schutt","year":"2010","unstructured":"Schutt, A., Stuckey, P.J.: Incremental satisfiability and implication for utvpi constraints. INFORMS J. Comput. 22(4), 514\u2013527 (2010)","journal-title":"INFORMS J. Comput."},{"issue":"2","key":"20_CR16","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s10817-009-9139-4","volume":"43","author":"K Subramani","year":"2009","unstructured":"Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Autom. Reasoning (JAR) 43(2), 121\u2013137 (2009)","journal-title":"J. Autom. Reasoning (JAR)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25150-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T20:17:07Z","timestamp":1748636227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25150-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319251493","9783319251509"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25150-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}