{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:04:31Z","timestamp":1743073471071,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642157684"},{"type":"electronic","value":"9783642157691"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_11","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T06:09:40Z","timestamp":1284358180000},"page":"167-183","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Abstraction for Intervals Using Boolean Formulae"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Brauer","sequence":"first","affiliation":[]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Atmel Corporation. The Atmel 8-bit AVR Microcontroller with 16K Bytes of In-system Programmable Flash (2009), \n                    http:\/\/www.atmel.com\/atmel\/acrobat\/doc2466.pdf"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G.: WYSINWYX: What You See Is Not What You eXecute. PhD thesis, Computer Sciences Department, University of Wisconsin, Madison, Wisconsin, USA (August 2007)","DOI":"10.1007\/978-3-540-69149-5_22"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","first-page":"395","volume-title":"Verification: Theory and Practice","author":"V. Chandru","year":"2004","unstructured":"Chandru, V., Lassez, J.-L.: Qualitative Theorem Proving in Linear Constraints. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 395\u2013406. Springer, Heidelberg (2004)"},{"key":"11_CR4","volume-title":"Linear Programming","author":"V. Chv\u00e1tal","year":"1983","unstructured":"Chv\u00e1tal, V.: Linear Programming. W.\u00a0H.\u00a0Freeman and Company, New York (1983)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"11_CR6","first-page":"238","volume-title":"POPL","author":"P. Cousot","year":"1977","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. ACM Press, New York (1977)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening\/Narrowing Approaches to Abstract Interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"11_CR8","first-page":"84","volume-title":"POPL","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: POPL, pp. 84\u201397. ACM Press, New York (1978)"},{"issue":"2","key":"11_CR9","first-page":"203","volume":"32","author":"J. Edmonds","year":"1997","unstructured":"Edmonds, J., Manrras, J.-F.: Note sur les Q-matrices d\u2019Edmonds. Recherche Op\u00e9rationnella\u00a032(2), 203\u2013209 (1997)","journal-title":"Recherche Op\u00e9rationnella"},{"issue":"13","key":"11_CR10","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1080\/00207168908803778","volume":"30","author":"P. Granger","year":"1989","unstructured":"Granger, P.: Static Analysis of Arithmetical Congruences. International Journal of Computer Mathematics\u00a030(13), 165\u2013190 (1989)","journal-title":"International Journal of Computer Mathematics"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0032748","volume-title":"Static Analysis","author":"P. Granger","year":"1997","unstructured":"Granger, P.: Static Analyses of Congruence Properties on Rational Numbers. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302, pp. 278\u2013292. Springer, Heidelberg (1997)"},{"key":"11_CR12","first-page":"281","volume-title":"PLDI","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program Analysis as Constraint Solving. In: PLDI, pp. 281\u2013292. ACM Press, New York (2008)"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine Relationships among Variables of a Program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-11319-2_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. King","year":"2010","unstructured":"King, A., S\u00f8ndergaard, H.: Automatic Abstraction for Congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 197\u2013213. Springer, Heidelberg (2010)"},{"key":"11_CR15","volume-title":"Decision Procedures","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)"},{"key":"11_CR16","unstructured":"Le Berre, D.: SAT4J: Bringing the power of SAT technology to the Java platform (2010), \n                    http:\/\/www.sat4j.org\/"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BF01178576","volume":"30","author":"K. Marriott","year":"1993","unstructured":"Marriott, K.: Frameworks for Abstract Interpretation. Acta Informatica\u00a030(2), 103\u2013129 (1993)","journal-title":"Acta Informatica"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"issue":"1","key":"11_CR19","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. Higher-Order and Symbolic Computation\u00a019(1), 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"11_CR20","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1145\/1480881.1480899","volume-title":"POPL","author":"D. Monniaux","year":"2009","unstructured":"Monniaux, D.: Automatic Modular Abstractions for Linear Constraints. In: POPL, pp. 140\u2013151. ACM Press, New York (2009)"},{"key":"11_CR21","unstructured":"Monniaux, D.: Personal communication with Monniaux at VMCAI (January 2010)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1016","DOI":"10.1007\/978-3-540-27836-8_85","volume-title":"Automata, Languages and Programming","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: A Note on Karr\u2019s Algorithm. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 1016\u20131028. Springer, Heidelberg (2004)"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of Modular Arithmetic. ACM Trans. Program. Lang. Syst.\u00a029(5) (August 2007)","DOI":"10.1145\/1275497.1275504"},{"issue":"2","key":"11_CR24","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s10107-003-0433-3","volume":"99","author":"A. Neumaier","year":"2004","unstructured":"Neumaier, A., Shcherbina, O.: Safe Bounds in Linear and Mixed-Integer Linear Programming. Math. Program.\u00a099(2), 283\u2013296 (2004)","journal-title":"Math. Program."},{"issue":"3","key":"11_CR25","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation\u00a02(3), 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"issue":"5","key":"11_CR26","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1037949.1024410","volume":"38","author":"J. Regehr","year":"2004","unstructured":"Regehr, J., Reid, A.: HOIST: A System for Automatically Deriving Static Analyzers for Embedded Systems. ACM SIGOPS Operating Systems Review\u00a038(5), 133\u2013143 (2004)","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic Implementation of the Best Transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constraint based linear relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 53\u201368. Springer, Heidelberg (2004)"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-74061-2_8","volume-title":"Static Analysis","author":"A. Simon","year":"2007","unstructured":"Simon, A., King, A.: Taming the Wrapping of Integer Arithmetic. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 121\u2013136. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:32:29Z","timestamp":1676691149000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}