Abstract interpretation of microcontroller code: Intervals meet congruences

Citations of this article
Mendeley users who have this article in their library.


Bitwise instructions, loops and indirect data access present challenges to the verification of microcontroller programs. In particular, since registers are often memory mapped, it is necessary to show that an indirect store operation does not accidentally mutate a register. To prove this and related properties, this article advocates using the domain of bitwise linear congruences in conjunction with intervals to derive accurate range information. The paper argues that these two domains complement one another when reasoning about microcontroller code. The paper also explains how SAT solving, which applied with dichotomic search, can be used to recover branching conditions from binary code which, in turn, further improves interval analysis. © 2011 Elsevier B.V. All rights reserved.




Brauer, J., King, A., & Kowalewski, S. (2013). Abstract interpretation of microcontroller code: Intervals meet congruences. In Science of Computer Programming (Vol. 78, pp. 862–883). https://doi.org/10.1016/j.scico.2012.06.001

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free