Range analysis of microcontroller code using bit-level congruences
FREE-DOWNLOAD J Brauer, A King… – Formal Methods for Industrial Critical …, 2010 –
Abstract. Bitwise instructions, loops and indirect data access pose dif- ficult challenges to the
verification of microcontroller programs. In par- ticular, it is necessary to show that an indirect
write does not mutate registers, which are indirectly addressable. To prove this property, .