{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:07:12Z","timestamp":1763968032144},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642158971"},{"type":"electronic","value":"9783642158988"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-15898-8_6","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T09:43:47Z","timestamp":1284371027000},"page":"82-98","source":"Crossref","is-referenced-by-count":3,"title":["Range Analysis of Microcontroller Code Using Bit-Level Congruences"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Brauer","sequence":"first","affiliation":[]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Kowalewski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Atmel Corporation. 8-bit AVR Instruction Set (July 2008)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-71410-1_16","volume-title":"Logic-Based Program Synthesis and Transformation","author":"R. Bagnara","year":"2007","unstructured":"Bagnara, R., Dobson, K., Hill, P., Mundell, M., Zaffanella, E.: Grids: A domain for analyzing the distribution of numerical values. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 219\u2013235. Springer, Heidelberg (2007)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.W.: WYSINWYX: What You See Is Not What You eXecute. ACM Trans. Program. Lang. Syst. (to appear, 2010)","DOI":"10.1145\/1749608.1749612"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"SAS 2010","author":"J. Brauer","year":"2010","unstructured":"Brauer, J., King, A.: Automatic abstraction for intervals using boolean formulae. In: SAS 2010. LNCS. Springer, Heidelberg (2010)"},{"key":"6_CR5","volume-title":"SCOPES","author":"J. Brauer","year":"2010","unstructured":"Brauer, J., Noll, T., Schlich, B.: Interval analysis of microcontroller code using abstract interpretation of hardware and software. In: SCOPES. ACM, New York (to appear, 2010)"},{"issue":"1","key":"6_CR6","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1017\/S1471068407003146","volume":"8","author":"M. Codish","year":"2008","unstructured":"Codish, M., Lagoon, V., Stuckey, P.J.: Logic programming with Satisfiability. Theory and Practice of Logic Programming\u00a08(1), 121\u2013128 (2008)","journal-title":"Theory and Practice of Logic Programming"},{"issue":"1","key":"6_CR7","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/200994.200998","volume":"17","author":"M. Codish","year":"1995","unstructured":"Codish, M., Mulkers, A., Bruynooghe, M., Garc\u00eda de la Banda, M.J., Hermenegildo, M.V.: Improving abstract interpretations by combining domains. ACM Trans. Program. Lang. Syst.\u00a017(1), 28\u201344 (1995)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR8","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, New York (1977)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., Rival, X.: The Astr\u00e9e analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"6_CR11","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)"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1145\/1450058.1450093","volume-title":"EMSOFT","author":"E. Eide","year":"2008","unstructured":"Eide, E., Regehr, J.: Volatiles are miscompiled, and what to do about it. In: EMSOFT, pp. 255\u2013264. ACM, New York (2008)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-53982-4_10","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"P. Granger","year":"1991","unstructured":"Granger, P.: Static analysis of linear congruence equalities among variables of a program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol.\u00a0493, pp. 169\u2013192. Springer, Heidelberg (1991)"},{"key":"6_CR14","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1145\/1328438.1328468","volume-title":"POPL","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246. ACM, New York (2008)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-70545-1_26","volume-title":"Computer Aided Verification","author":"A. King","year":"2008","unstructured":"King, A., S\u00f8ndergaard, H.: Inferring congruence equations using SAT. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 281\u2013293. Springer, Heidelberg (2008)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/978-3-642-15037-1","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. 281\u2013293. Springer, Heidelberg (2010)"},{"issue":"1","key":"6_CR17","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":"6_CR18","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"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-540-77966-7_16","volume-title":"Hardware and Software: Verification and Testing","author":"T. Noll","year":"2008","unstructured":"Noll, T., Schlich, B.: Delayed nondeterminism in model checking embedded systems assembly code. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 185\u2013201. Springer, Heidelberg (2008)"},{"issue":"5","key":"6_CR20","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. Operating Systems Review\u00a038(5), 133\u2013143 (2004)","journal-title":"Operating Systems Review"},{"key":"6_CR21","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":"6_CR22","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","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15898-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T08:03:02Z","timestamp":1685779382000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15898-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642158971","9783642158988"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15898-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}