{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T15:55:03Z","timestamp":1775145303027,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319522333","type":"print"},{"value":"9783319522340","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_27","type":"book-chapter","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T04:52:06Z","timestamp":1484110326000},"page":"500-520","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Sound Bit-Precise Numerical Domains"],"prefix":"10.1007","author":[{"given":"Tushar","family":"Sharma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"issue":"4\/5","key":"27_CR1","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/s10009-005-0215-8","volume":"8","author":"R Bagnara","year":"2006","unstructured":"Bagnara, R., Hill, P., Zaffanella, E.: Widening operators for powerset domains. STTT 8(4\/5), 449\u2013466 (2006)","journal-title":"STTT"},{"issue":"1\u20132","key":"27_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"27_CR3","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1145\/1749608.1749612","volume":"32","author":"G Balakrishnan","year":"2010","unstructured":"Balakrishnan, G., Reps, T.: WYSINWYX: what you see is not what you execute. TOPLAS 32(6), 202\u2013213 (2010)","journal-title":"TOPLAS"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_31"},{"key":"27_CR5","unstructured":"Bloch, J.: Extra, extra - read all about it: nearly all binary searches and mergesorts are broken. googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all- about-it-nearly.html"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-15769-1_11","volume-title":"Static Analysis","author":"J Brauer","year":"2010","unstructured":"Brauer, J., King, A.: Automatic abstraction for intervals using boolean formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 167\u2013183. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15769-1_11"},{"issue":"3","key":"27_CR7","first-page":"63","volume":"8","author":"J Brauer","year":"2012","unstructured":"Brauer, J., King, A.: Transfer function synthesis without quantifier elimination. LMCS 8(3), 63 (2012)","journal-title":"LMCS"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Bygde, S., Lisper, B., Holsti, N.: Fully bounded polyhedral analysis of integers with wrapping. In: International Workshop on Numerical and Symbolic Abstract Domains (2011)","DOI":"10.1016\/j.entcs.2012.10.003"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of 2nd International Symposium on Programming, Paris, April 1976","DOI":"10.1145\/390018.808314"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: POPL (1978)","DOI":"10.1145\/512760.512770"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Dietz, W., Li, P., Regehr, J., Adve, V.: Understanding integer overflow in C\/C++. In: ICSE (2012)","DOI":"10.1109\/ICSE.2012.6227142"},{"key":"27_CR12","unstructured":"dSPACE TargetLink. www.dspace.com\/en\/pub\/home\/products\/sw\/pcgs\/targetli.cfm"},{"issue":"4","key":"27_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2651361","volume":"36","author":"M Elder","year":"2014","unstructured":"Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.: Abstract domains of affine relations. TOPLAS 36(4), 1\u201313 (2014)","journal-title":"TOPLAS"},{"issue":"4","key":"27_CR14","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1109\/TC.1978.1675101","volume":"27","author":"HL Garner","year":"1978","unstructured":"Garner, H.L.: Theory of computer addition and overflow. IEEE Trans. Comput. 27(4), 297\u2013301 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Ivan\u010di\u0107, F., Balakrishnan, G., Maeda, N., Gupta, A.: Donut domains: efficient non-convex domains for abstract interpretation. In: VMCAI (2012)","DOI":"10.1007\/978-3-642-27940-9_16"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Jones, N., Mycroft, A.: Data flow analysis of applicative programs using minimal function graphs. In: POPL, pp. 296\u2013306 (1986)","DOI":"10.1145\/512644.512672"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL (2015)","DOI":"10.1145\/2676726.2676966"},{"key":"27_CR18","unstructured":"Kidd, N., Lal, A., Reps, T.: WALi: the weighted automaton library (2007). www.cs.wisc.edu\/wpis\/wpds\/download.php"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/11513988_44","volume-title":"Computer Aided Verification","author":"A Lal","year":"2005","unstructured":"Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 434\u2013448. Springer, Heidelberg (2005). doi: 10.1007\/11513988_44"},{"key":"27_CR20","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: International Symposium on Code Generation and Optimization (2004)"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Laviron, V., Logozzo, F.: Subpolyhedra: a (more) scalable approach to infer linear inequalities. In: VMCAI (2009)","DOI":"10.1007\/978-3-540-93900-9_20"},{"key":"27_CR22","unstructured":"Lim, J.: Transformer specification language: a system for generating analyzers and its applications. Ph.D. thesis, Computer Science Department, University of Wisconsin, Madison, WI, Technical report 1689, May 2011"},{"key":"27_CR23","unstructured":"LLVM: Low level virtual machine. llvm.org"},{"key":"27_CR24","unstructured":"Malmkj\u00e6r, K.: Abstract interpretation of partial-evaluation algorithms. Ph.D. thesis, Department of Computer and Information Science, Kansas State University, Manhattan, Kansas (1993)"},{"issue":"1","key":"27_CR25","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"1006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order Symbolic Comput. 19(1), 31\u2013100 (1006)","journal-title":"Higher-Order Symbolic Comput."},{"key":"27_CR26","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE (2001)"},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117\u2013132. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45789-5_11"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Abstract domains for bit-level machine integer and floating-point operations. In: IJCAR, pp. 55\u201370 (2012)","DOI":"10.29007\/b63g"},{"issue":"3","key":"27_CR29","first-page":"4","volume":"6","author":"D Monniaux","year":"2010","unstructured":"Monniaux, D.: Automatic modular abstractions for template numerical constraints. LMCS 6(3), 4 (2010)","journal-title":"LMCS"},{"issue":"5","key":"27_CR30","doi-asserted-by":"publisher","first-page":"29:1","DOI":"10.1145\/1275497.1275504","volume":"29","author":"M M\u00fcller-Olm","year":"2007","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. TOPLAS 29(5), 29:1\u201329:27 (2007)","journal-title":"TOPLAS"},{"key":"27_CR31","doi-asserted-by":"crossref","unstructured":"Mycroft, A., Jones, N.: A relational framework for abstract interpretation. In: Programs as Data Objects (1985)","DOI":"10.1007\/3-540-16446-4_9"},{"key":"27_CR32","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(89)90091-1","volume":"69","author":"F Nielson","year":"1989","unstructured":"Nielson, F.: Two-level semantics and abstract interpretation. Theor. Comp. Sci. 69, 117\u2013242 (1989)","journal-title":"Theor. Comp. Sci."},{"key":"27_CR33","unstructured":"PPL: The Parma polyhedra library. www.cs.unipr.it\/ppl\/"},{"key":"27_CR34","doi-asserted-by":"crossref","unstructured":"Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: PEPM (2006)","DOI":"10.1145\/1111542.1111560"},{"issue":"1\u20132","key":"27_CR35","first-page":"206","volume":"58","author":"T Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP 58(1\u20132), 206\u2013263 (2005)","journal-title":"SCP"},{"key":"27_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11823230_2","volume-title":"Static Analysis","author":"S Sankaranarayanan","year":"2006","unstructured":"Sankaranarayanan, S., Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3\u201317. Springer, Berlin (2006). doi: 10.1007\/11823230_2"},{"key":"27_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25\u201341. Springer, Berlin (2005). doi: 10.1007\/978-3-540-30579-8_2"},{"key":"27_CR38","doi-asserted-by":"crossref","unstructured":"Sen, R., Srikant, Y.: Executable analysis using abstract interpretation with circular linear progressions. In: MEMOCODE (2007)","DOI":"10.1109\/MEMCOD.2007.371251"},{"key":"27_CR39","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications. Prentice-Hall (1981)"},{"key":"27_CR40","unstructured":"Sharma, T., Thakur, A., Reps, T.: An abstract domain for bit-vector inequalities. TR-1789, Computer Science Department, University of Wisconsin, Madison, WI (2013)"},{"key":"27_CR41","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: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 121\u2013136. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74061-2_8"},{"key":"27_CR42","doi-asserted-by":"crossref","unstructured":"Simon, A., King, A., Howe, J.: Two variables per linear inequality as an abstract domain. In: International Workshop on Logic Based Program Development and Transformation, pp. 71\u201389 (2002)","DOI":"10.1007\/3-540-45013-0_7"},{"key":"27_CR43","volume-title":"Hacker\u2019s Delight","author":"H Warren Jr","year":"2003","unstructured":"Warren Jr., H.: Hacker\u2019s Delight. Addison-Wesley, Boston (2003)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T07:45:10Z","timestamp":1749887110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"12 January 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/conf.researchr.org\/home\/VMCAI-2017","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}