A better x86 memory model: x86-TSO S Owens, S Sarkar, P Sewell Theorem Proving in Higher Order Logics, 391-407 | 130 | ∗ | 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 | 111 | | 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 | 98 | | 2009 |

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 | 75 | | 2007 |

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

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

Regular-expression derivatives re-examined. S Owens, JH Reppy, A Turon J. Funct. Program. 19 (2), 173-190 | 50 | | 2009 |

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 | 48 | | 2010 |

Reasoning about the implementation of concurrency abstractions on x86-TSO S Owens ECOOP 2010–Object-Oriented Programming, 478-503 | 43 | | 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 | 31 | | 2012 |

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 | 30 | ∗ | 2007 |

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

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

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 | 18 | | 2006 |

Functional correctness proofs of encryption algorithms J Duan, J Hurd, G Li, S Owens, K Slind, J Zhang LPAR 3835, 519-533 | 16 | | 2005 |

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 | 15 | | 2012 |

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

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

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 | 11 | | 2012 |

Adapting functional programs to higher order logic S Owens, K Slind Higher-Order and Symbolic Computation 21 (4), 377-409 | 11 | | 2008 |