The semantics of x86-CC multiprocessor machine code S Sarkar, P Sewell, FZ Nardelli, S Owens, T Ridge, T Braibant, ... ACM SIGPLAN Notices 44 (1), 379-391, 2009 | 210 | 2009 |
Ott: Effective tool support for the working semanticist P Sewell, FZ Nardelli, S Owens, G Peskine, T Ridge, S Sarkar, R Strniša Journal of Functional Programming 20 (1), 71, 2010 | 207 | 2010 |
Ott: Effective tool support for the working semanticist P Sewell, FZ Nardelli, S Owens, G Peskine, T Ridge, S Sarkar, R Strniša ACM SIGPLAN Notices 42 (9), 1-12, 2007 | 134 | 2007 |
Lem: reusable engineering of real-world semantics DP Mulligan, S Owens, KE Gray, T Ridge, P Sewell ACM SIGPLAN Notices 49 (9), 175-188, 2014 | 121 | 2014 |
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems T Ridge, D Sheets, T Tuerk, A Giugliano, A Madhavapeddy, P Sewell Proceedings of the 25th Symposium on Operating Systems Principles, 38-53, 2015 | 82 | 2015 |
The 1st verified software competition: Experience report V Klebanov, P Müller, N Shankar, GT Leavens, V Wüstholz, E Alkassar, ... International Symposium on Formal Methods, 154-168, 2011 | 79 | 2011 |
A mechanically verified, sound and complete theorem prover for first order logic T Ridge, J Margetson International Conference on Theorem Proving in Higher Order Logics, 294-309, 2005 | 69 | 2005 |
A rely-guarantee proof system for x86-TSO T Ridge Verified Software: Theories, Tools, Experiments: Third International …, 2010 | 56 | 2010 |
Simple, functional, sound and complete parsing for all context-free grammars T Ridge Certified Programs and Proofs, 2011, 2011 | 41 | 2011 |
Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the Sockets API S Bishop, M Fairbairn, H Mehnert, M Norrish, T Ridge, P Sewell, M Smith, ... Journal of the ACM (JACM) 66 (1), 1-77, 2018 | 24 | 2018 |
Verifying distributed systems: the operational approach T Ridge Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2009 | 22 | 2009 |
A rigorous approach to networking: TCP, from implementation to protocol to service T Ridge, M Norrish, P Sewell FM 2008: Formal Methods: 15th International Symposium on Formal Methods …, 2008 | 22 | 2008 |
Rigorous protocol design in practice: An optical packet-switch MAC in HOL A Biltcliffe, M Dales, S Jansen, T Ridge, P Sewell Proceedings of the 2006 IEEE International Conference on Network Protocols …, 2006 | 13 | 2006 |
A mechanically verified, efficient, sound and complete theorem prover for first order logic T Ridge Archive of Formal Proofs, 2004 | 13 | 2004 |
TCP, UDP, and Sockets: Volume 3: The Service-level Specification T Ridge, M Norrish, P Sewell University of Cambridge, Computer Laboratory, 2009 | 11 | 2009 |
Operational reasoning for concurrent Caml programs and weak memory models T Ridge International Conference on Theorem Proving in Higher Order Logics, 278-293, 2007 | 11 | 2007 |
Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL T Ridge arXiv preprint cs/0607058, 2006 | 9 | 2006 |
Completeness theorem J Margetson, T Ridge Archive of Formal Proofs. http://afp. sf. net/entries/Completeness. shtml, 2004 | 9 | 2004 |
Simple, efficient, sound-and-complete combinator parsing for all context-free grammars, using an oracle T Ridge SLE 2014, 2014 | 8 | 2014 |
A mechanically verified, efficient, sound and complete theorem prover for first order logic. Archive of Formal Proofs (2004) T Ridge | 8 | 2004 |