Deprecated : The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Publications by Scott Owens
Publications by Scott Owens Multi-core Memory Models An Axiomatic Memory Model for POWER Multiprocessors Sela Mador-Haim , Luc Maranget , Susmit Sarkar , Kayvan Memarian, Jade Alglave , Scott Owens, Rajeev Alur , Milo M. K. Martin , Peter Sewell , Derek WilliamsCAV 2012 (bibtex ) (definitive version )Synchronising C/C++ and POWER Susmit Sarkar , Kayvan Memarian, Scott Owens, Mark Batty , Peter Sewell , Luc Maranget , Jade Alglave , Derek WilliamsPLDI 2012 (bibtex ) (author's local version )Clarifying and Compiling C/C++ Concurrency: From C++11 to POWER Mark Batty , Kayvan Memarian, Scott Owens, Susmit Sarkar , Peter Sewell POPL 2012 (bibtex ) (author's local version )Nitpicking C++ Concurrency Jasmin Christian Blanchette , Tjark Weber , Mark Batty , Scott Owens, Susmit Sarkar PPDP 2011 (bibtex ) (author's local version )Mathematizing C++ Concurrency Mark Batty , Scott Owens, Susmit Sarkar , Peter Sewell , Tjark Weber POPL 2011 (bibtex ) (author's local version )Mathematizing C++ Concurrency: The Post-Rapperswil Model Mark Batty , Scott Owens, Susmit Sarkar , Peter Sewell , Tjark Weber Technical report (bibtex )x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors Peter Sewell , Susmit Sarkar , Scott Owens, Francesco Zappa Nardelli , Magnus O. Myreen CACM , 53(7), July 2010 (bibtex ) (author's local version )Reasoning about the Implementation of Concurrency Abstractions on x86-TSO Scott OwensECOOP 2010 (bibtex ) (definitive version )Full proofs A Better x86 Memory Model: x86-TSO Scott Owens, Susmit Sarkar , Peter Sewell TPHOLs 2009 (bibtex ) (definitive version )Relaxed Memory Models Must Be Rigorous Francesco Zappa Nardelli , Peter Sewell , Jaroslav Sevcik, Susmit Sarkar , Scott Owens, Luc Maranget , Mark Batty , Jade Alglave EC2 2009 (bibtex )A Better x86 Memory Model: x86-TSO (Extended Version) Scott Owens, Susmit Sarkar , Peter Sewell Technical report (bibtex )The Semantics of x86-CC Multiprocessor Machine Code Susmit Sarkar , Peter Sewell , Francesco Zappa Nardelli , Scott Owens, Tom Ridge , Thomas Braibant , Magnus O. Myreen , Jade Alglave POPL 2009 (bibtex ) (author's local version )Mechanised Semantics Lem: A Lightweight Tool for Heavyweight Semantics Scott Owens, Peter Boehm , Francesco Zappa Nardelli , Peter Sewell ITP 2011 ("Rough Diamond" section) (bibtex ) (definitive version )Lem's homepage Ott or Nott Stephanie Weirich , Scott Owens, Peter Sewell , Francesco Zappa Nardelli WMM 2010 (bibtex )Ott: Effective Tool Support for the Working Semanticist Peter Sewell , Francesco Zappa Nardelli , Scott Owens, Gilles Peskine , Thomas Ridge , Susmit Sarkar , Rok Strnisa JFP , 20(1), January 2010 (bibtex ) (definitive version ) See also the Ott web page . (Copyright Cambridge University Press)A Sound Semantics for OCaml light Scott OwensESOP 2008 (bibtex ) (definitive version )Ott: Effective Tool Support for the Working Semanticist Peter Sewell , Francesco Zappa Nardelli , Scott Owens, Gilles Peskine , Thomas Ridge , Susmit Sarkar , Rok Strnisa ICFP 2007 (bibtex ) (author's local version )Verifying Type Soundness for OCaml: The Core Language Scott Owens, Gilles Peskine WMM 2007 (bibtex )Theorem Proving Proof-producing translation of higher-order logic into pure and stateful MLMagnus O. Myreen , Scott OwensJFP (bibtex ) Steps Towards Verified Implementations of HOL Light Magnus O. Myreen , Scott Owens, Ramana Kumar ITP 2013 ("Rough Diamond" section) (bibtex ) (definitive version )Proof-Producing Synthesis of ML from Higher-Order Logic Magnus O. Myreen , Scott OwensICFP 2012 (bibtex ) (author's local version )Compiling Higher Order Logic by Proof Konrad Slind, Guodong Li , Scott Owens Book chapter in Design and Verification of Microprocessor Systems for High-Assurance Applications (bibtex ) (definitive version ) Adapting Functional Programs to Higher-Order Logic Scott Owens, Konrad SlindHOSC , 21(4), December 2008 (bibtex ) (definitive version ) Proof Producing Synthesis of Arithmetic and Cryptographic Hardware Konrad Slind, Scott Owens, Juliano Iyoda , Mike Gordon FAC , 19(3), August 2007 (bibtex ) (definitive version ) Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic Guodong Li , Scott Owens, Konrad SlindESOP 2007 (bibtex ) (definitive version )Automatic Formal Synthesis of Hardware from Higher Order Logic Mike Gordon , Juliano Iyoda , Scott Owens, Konrad SlindAVoCS 2005 (bibtex ) (definitive version )Functional Correctness Proofs of Encryption Algorithms Jianjun Duan, Joe Hurd , Guodong Li , Scott Owens, Konrad Slind, Junxing Zhang LPAR 2005 (bibtex ) (definitive version )A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic Mike Gordon , Juliano Iyoda , Scott Owens, Konrad SlindTPHOLs 2005, emerging trends (bibtex )Proving as Programming with DrHOL: A Preliminary Design Scott Owens, Konrad SlindUITP 2003 (bibtex )Module Systems Compiler Front-ends Validate XHTML 1.0 Strict Validate CSS