School of Computing

Range Analysis of Microcontroller Code Using Bit-Level Congruences

Jorg Brauer, Andy King, and Stefan Kowalewski

In Stefan Kowalewski and Marco Roveri, editors, Formal Methods for Industrial Critical Systems, volume 6371 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, September 2010.

Abstract

Verifying the correctness of microcontroller programs in presence of bitwise instructions, loops, and indirect data access poses difficult challenges. 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.

Download publication 285 kbytes (PDF)

Bibtex Record

@inproceedings{3053,
author = {Jorg Brauer and Andy King and Stefan Kowalewski},
title = {Range {A}nalysis of {M}icrocontroller {C}ode {U}sing {B}it-{L}evel {C}ongruences},
month = {September},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2010/3053},
    publication_type = {inproceedings},
    submission_id = {1701_1287400281},
    ISBN = {978-3-642-15897-1},
    booktitle = {Formal Methods for Industrial Critical Systems},
    editor = {Stefan Kowalewski and Marco Roveri },
    volume = {6371},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer-Verlag},
    refereed = {yes},
}

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

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

Last Updated: 21/03/2014