9 citations · 15 across the 12 of their papers we have counts for
Showing 2013Show all
3 papers · 1 filter
cs.LO2013
Soundness and Completeness of the NRB Verification Logic
Peter T. Breuer, Simon J. Pickin
This short paper gives a model for and a proof of completeness of the NRB verification logic for deterministic imperative programs, the logic having been used in the past as the ba…
cs.CR2013
An Open Question on the Uniqueness of (Encrypted) Arithmetic
Peter T. Breuer, Jonathan P. Bowen
We ask whether two or more images of arithmetic may inhabit the same space via different encodings. The answers have significance for a class of processor design that does all its…
cs.LO2013★ 2 cited
Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky
Peter T. Breuer, Jonathan P. Bowen
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 beca…