School of Computing

Abstract Interpretation of Microcontroller Code: Intervals meet Congruences

J"org Brauer, Andy King, and Stefan Kowalewski

Science of Computer Programming, 77, July 2012 [doi].


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 accidently mutate a register. To prove this and related properties, this article advocates using the domain of bit-wise 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.

Download publication 247 kbytes (PDF)

Bibtex Record

author = {J"{o}rg Brauer and Andy King and Stefan Kowalewski},
title = {Abstract {I}nterpretation of {M}icrocontroller {C}ode: {I}ntervals meet {C}ongruences},
month = {July},
year = {2012},
pages = {},
keywords = {},
note = {},
doi = {10.1016/j.scico.2012.06.001},
url = {},
    publication_type = {article},
    submission_id = {3943_1343824912},
    journal = {Science of Computer Programming},
    volume = {77},
    publisher = {Elsevier},

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014