Changeset 2370


Ignore:
Timestamp:
Sep 28, 2012, 4:19:25 PM (7 years ago)
Author:
mulligan
Message:

Added reference to Jaap's ArXiv? paper

Location:
Papers/cpp-asm-2012
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.bib

    r2362 r2370  
    9595
    9696@inproceedings
    97 { boender:correctness:2012,
    98   author = {Jaap Boender and Claudio {Sacerdoti Coen}},
    99   title = {On the correctness of a branch displacement algorithm},
    100   booktitle = {{CPP}},
    101   year =  {2012},
    102   note = {Submitted}
    103 }
    104 
    105 @inproceedings
    10697{ fox:trustworthy:2010,
    10798  author = {Anthony Fox and Magnus O. Myreen},
     
    175166
    176167@misc
     168{ boender:correctness:2012,
     169  author = {Jaap Boender and Claudio {Sacerdoti Coen}},
     170  title = {On the correctness of a branch displacement algorithm},
     171  howpublished = {\url{http://arxiv.org/abs/1209.5920}},
     172  year = {2012}
     173}
     174
     175@misc
    177176{ cerco:2011,
    178177  title = {The {CerCo} {FET-Open} project},
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2369 r2370  
    521521\label{subsect.total.correctness.for.well.behaved.assembly.programs}
    522522
    523 The traditional approach to verifying the correctness of an assembler is to
    524 restrict the semantics of assembly code to treat memory addresses as opaque
    525 (symbolic) structures that cannot be modified.
    526 Memory is represented as a map from opaque addresses to the disjoint union of data and opaque addresses---addresses are kept opaque to prevent their possible `semantics breaking' manipulation by assembly programs:
     523The traditional approach to verifying the correctness of an assembler is to restrict the semantics of assembly code so that it treats memory addresses as opaque (symbolic) structures that cannot be modified.
     524Memory is then represented as a map from opaque addresses to the disjoint union of data and opaque addresses---addresses are kept opaque to prevent their possible `semantics breaking' manipulation by assembly programs:
    527525\begin{displaymath}
    528526\mathtt{Mem} : \mathtt{Addr} \rightarrow \mathtt{Bytes} + \mathtt{Addr} \qquad \llbracket - \rrbracket : \mathtt{Instr} \rightarrow \mathtt{Mem} \rightarrow \mathtt{option\ Mem}
Note: See TracChangeset for help on using the changeset viewer.