Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky
Conference item
Breuer, PT and Bowen, JP (2013). Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky. International Conference on Software Engineering and Formal Methods. Madrid, Spain London South Bank University. https://doi.org/10.1007/978-3-319-05032-4_27
Authors | Breuer, PT and Bowen, JP |
---|---|
Abstract | Sometimes machine code turns out to be a better target for verification than source code. RISC machine code is especially advantaged with respect to source code in this regard because it has only two instructions that access memory. That architecture forms the basis here for an inference system that can prove machine code safe against `hardware aliasing', an effect that occurs in embedded systems. There are programming memes that ensure code is safe from hardware aliasing, but we want to certify that a given machine code is provably safe. |
Year | 2013 |
Publisher | London South Bank University |
Digital Object Identifier (DOI) | https://doi.org/10.1007/978-3-319-05032-4_27 |
Accepted author manuscript | License File description Conference Paper |
Publication dates | |
23 Sep 2013 | |
Publication process dates | |
Deposited | 20 Dec 2016 |
Permalink -
https://openresearch.lsbu.ac.uk/item/878wz
Download files
89
total views147
total downloads2
views this month0
downloads this month