Search the dblp DataBase

Publications of Author

1. Magnus O. Myreen, Michael J. C. Gordon
   Hoare Logic for Realistically Modelled Machine Code. [Citation Graph (0, 0)][DBLP]
   TACAS, 2007, pp:568-582 [Conf]
   
2. Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
   Hoare Logic for ARM Machine Code. [Citation Graph (0, 0)][DBLP]
   FSEN, 2007, pp:272-286 [Conf]
   
3. 
   Extensible Proof-Producing Compilation. [Citation Graph (, )][DBLP]
   
   
4. 
   Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. [Citation Graph (, )][DBLP]
   
   
5. 
   The semantics of x86-CC multiprocessor machine code. [Citation Graph (, )][DBLP]
   
   
6. 
   Verified just-in-time compiler on x86. [Citation Graph (, )][DBLP]
   
   
7. 
   The semantics of power and ARM multiprocessor machine code. [Citation Graph (, )][DBLP]
   
   
8. 
   Verified LISP Implementations on ARM, x86 and PowerPC. [Citation Graph (, )][DBLP]
   
   
9. 
   Reusable Verification of a Copying Collector. [Citation Graph (, )][DBLP]
   
   
10. 
    A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. [Citation Graph (, )][DBLP]
    
    
11. 
    Separation Logic Adapted for Proofs by Rewriting. [Citation Graph (, )][DBLP]
    
    
12. 
    x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. [Citation Graph (, )][DBLP]
    
    
13. 
    Transforming Programs into Recursive Functions. [Citation Graph (, )][DBLP]