Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky

Peter Breuer

doi:10.1007/978-3-319-05032-4_27

Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky

Peter Breuer

Research output: Contribution to conference › Item › peer-review

2 Citations (Scopus)

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.

Original language	English
DOIs	https://doi.org/10.1007/978-3-319-05032-4_27
Publication status	Published - 23 Sept 2013
Externally published	Yes
Event	International Conference on Software Engineering and Formal Methods - Duration: 23 Sept 2013 → …

Conference

Conference	International Conference on Software Engineering and Formal Methods
Period	23/09/13 → …

Access to Document

10.1007/978-3-319-05032-4_27Licence: CC BY-NC-ND 4.0

Cite this

@conference{3041ed7e2ce34462af434f0d087ffe53,

title = "Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky",

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.",

author = "Peter Breuer",

year = "2013",

month = sep,

day = "23",

doi = "10.1007/978-3-319-05032-4_27",

language = "English",

note = "International Conference on Software Engineering and Formal Methods ; Conference date: 23-09-2013",

}

TY - CONF

T1 - Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky

AU - Breuer, Peter

PY - 2013/9/23

Y1 - 2013/9/23

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-05032-4_27

DO - 10.1007/978-3-319-05032-4_27

M3 - Item

T2 - International Conference on Software Engineering and Formal Methods

Y2 - 23 September 2013

ER -

Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this