Skip to main content

Range Analysis of Microcontroller Code Using Bit-Level Congruences: 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. Proceedings

Brauer, Jorg and King, Andy and Kowalewski, Stefan (2010) Range Analysis of Microcontroller Code Using Bit-Level Congruences: 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. Proceedings. In: Kowalewski, Stefan and Roveri, Marco, eds. Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science, 6371 . Springer, pp. 82-98. ISBN 978-3-642-15897-1. (doi:10.1007/978-3-642-15898-8_6) (KAR id:37590)

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.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-642-15898-8_6
Subjects: A General Works
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 12 Dec 2013 21:22 UTC
Last Modified: 16 Nov 2021 10:14 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/37590 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.