Sciweavers

FMICS
2010
Springer

Range Analysis of Microcontroller Code Using Bit-Level Congruences

13 years 10 months ago
Range Analysis of Microcontroller Code Using Bit-Level Congruences
Bitwise instructions, loops and indirect data access pose difficult challenges to the verification of microcontroller programs. In particular, it is necessary to show that an indirect write does not mutate registers, which are indirectly addressable. To prove this property, among others, this paper presents a relational binary-code semantics and details how this can be used to compute program invariants in terms of bit-level congruences. Moreover, it demonstrates how congruences can be combined with intervals to derive accurate ranges, as well as information about strided indirect memory accesses.
Jörg Brauer, Andy King, Stefan Kowalewski
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where FMICS
Authors Jörg Brauer, Andy King, Stefan Kowalewski
Comments (0)