Brauer, J''org and King, Andy and Kowalewski, Stefan (2012) Abstract Interpretation of Microcontroller Code: Intervals meet Congruences. Science of Computer Programming, 77 .
| 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/2012/3245 |
Abstract
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.
| Item Type: | Article |
|---|---|
| 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: | Andy King |
| Date Deposited: | 21 Sep 2012 09:49 |
| Last Modified: | 21 Sep 2012 09:49 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/30802 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
