Brauer, Jorg and King, Andy and Kowalewski, Stefan (2010) Range Analysis of Microcontroller Code Using Bit-Level Congruences. In: Formal Methods for Industrial Critical Systems.
| The full text of this publication is not available from this repository. (Contact us about this Publication) | |
| Official URL http://www.cs.kent.ac.uk/pubs/2010/3053 |
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: | Conference or workshop item (UNSPECIFIED) |
|---|---|
| Uncontrolled keywords: | determinacy analysis, Craig interpolants |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group |
| Depositing User: | Anastasia Bakowski |
| Date Deposited: | 21 Sep 2012 09:49 |
| Last Modified: | 21 Sep 2012 09:49 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/30632 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
