A better x86 memory model: x86-TSO S Owens, S Sarkar, P Sewell Theorem Proving in Higher Order Logics, 391-407, 2009 | 151* | 2009 |

x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors P Sewell, S Sarkar, S Owens, F Zappa Nardelli, MO Myreen Communications of the ACM 53 (7), 89-97, 2010 | 129 | 2010 |

The semantics of x86-CC multiprocessor machine code S Sarkar, P Sewell, F Zappa Nardelli, S Owens, T Ridge, T Braibant, ... ACM SIGPLAN Notices 44 (1), 379-391, 2009 | 107 | 2009 |

Mathematizing C++ concurrency M Batty, S Owens, S Sarkar, P Sewell, T Weber ACM SIGPLAN Notices 46 (1), 55-66, 2011 | 80 | 2011 |

Ott: effective tool support for the working semanticist P Sewell, F Zappa Nardelli, S Owens, G Peskine, T Ridge, S Sarkar, ... ACM SIGPLAN Notices 42 (9), 1-12, 2007 | 77 | 2007 |

Deformable volumes in path planning applications E Anshelevich, S Owens, F Lamiraux, EE Kavraki Robotics and Automation, 2000. Proceedings. ICRA'00. IEEE International ..., 2000 | 68 | 2000 |

Ott: Effective tool support for the working semanticist P Sewell, F Zappa Nardelli, S Owens, G Peskine, T Ridge, S Sarkar, ... Journal of Functional Programming 20 (01), 71-122, 2010 | 64 | 2010 |

Regular-expression derivatives re-examined S Owens, J Reppy, A Turon Journal of Functional Programming 19 (02), 173-190, 2009 | 55 | 2009 |

Reasoning about the implementation of concurrency abstractions on x86-TSO S Owens ECOOP 2010–Object-Oriented Programming, 478-503, 2010 | 49 | 2010 |

Clarifying and compiling C/C++ concurrency: from C++ 11 to POWER M Batty, K Memarian, S Owens, S Sarkar, P Sewell ACM SIGPLAN Notices 47 (1), 509-520, 2012 | 35 | 2012 |

A sound semantics for OCaml light S Owens Programming Languages and Systems, 1-15, 2008 | 32 | 2008 |

Structure of a proof-producing compiler for a subset of higher order logic G Li, S Owens, K Slind Programming Languages and Systems, 205-219, 2007 | 30* | 2007 |

From structures and functors to modules and units S Owens, M Flatt ACM SIGPLAN Notices 41 (9), 87-98, 2006 | 30 | 2006 |

Automatic formal synthesis of hardware from higher order logic M Gordon, J Iyoda, S Owens, K Slind Electronic Notes in Theoretical Computer Science 145, 27-43, 2006 | 20 | 2006 |

Synchronising C/C++ and POWER S Sarkar, K Memarian, S Owens, M Batty, P Sewell, L Maranget, J Alglave, ... ACM SIGPLAN Notices 47 (6), 311-322, 2012 | 19 | 2012 |

An axiomatic memory model for POWER multiprocessors S Mador-Haim, L Maranget, S Sarkar, K Memarian, J Alglave, S Owens, ... Computer Aided Verification, 495-512, 2012 | 19 | 2012 |

Functional correctness proofs of encryption algorithms J Duan, J Hurd, G Li, S Owens, K Slind, J Zhang Logic for Programming, Artificial Intelligence, and Reasoning, 519-533, 2005 | 17 | 2005 |

Lexer and parser generators in Scheme S Owens, M Flatt, O Shivers, B McMullan Indiana University Department of Computer Science 600, 41-52, 2004 | 16 | 2004 |

Lem: A lightweight tool for heavyweight semantics S Owens, P Böhm, F Zappa Nardelli, P Sewell Interactive Theorem Proving, 363-369, 2011 | 15 | 2011 |

Proof producing synthesis of arithmetic and cryptographic hardware K Slind, S Owens, J Iyoda, M Gordon Formal Aspects of Computing 19 (3), 343-362, 2007 | 14 | 2007 |