Changeset 2352 for Papers/cpp-asm-2012


Ignore:
Timestamp:
Sep 26, 2012, 5:57:59 PM (7 years ago)
Author:
mulligan
Message:

Removed repeated references as suggested by the referee

File:
1 edited

Legend:

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

    r2351 r2352  
    622622
    623623Aside from their application in verified compiler projects such as CerCo, CompCert~\cite{leroy:formally:2009} and CompCertTSO~\cite{sevcik:relaxed-memory:2011}, verified assemblers such as ours could also be applied to the verification of operating system kernels.
    624 Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}.
     624Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009}.
    625625This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler and compiler.
    626626
     
    649649% piton
    650650We are not the first to consider the total correctness of an assembler for a non-trivial assembly language.
    651 Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996,moore:grand:2005}.
     651Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}.
    652652This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two high-level languages---a dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
    653653
    654654% jinja
    655 Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006,klein:machine:2010}.
     655Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006}.
    656656They provide a compiler, virtual machine and operational semantics for the programming language and virtual machine, and prove that their compiler is semantics and type preserving.
    657657
Note: See TracChangeset for help on using the changeset viewer.