Tom Ridge
TitleCited byYear
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
1582009
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
1402010
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
982007
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
612014
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
592011
Jade Alglave, The semantics of x86-CC multiprocessor machine code
S Sarkar, P Sewell, FZ Nardelli, S Owens, T Ridge, T Braibant, ...
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2009
572009
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
462005
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
412015
A rely-guarantee proof system for x86-TSO
T Ridge
International Conference on Verified Software: Theories, Tools, and …, 2010
372010
Simple, functional, sound and complete parsing for all context-free grammars
T Ridge
Certified Programs and Proofs, 2011, 2011
252011
Verifying distributed systems: the operational approach
T Ridge
ACM SIGPLAN Notices 44 (1), 429-440, 2009
212009
A rigorous approach to networking: TCP, from implementation to protocol to service
T Ridge, M Norrish, P Sewell
International Symposium on Formal Methods, 294-309, 2008
202008
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
132006
A mechanically verified, efficient, sound and complete theorem prover for first order logic
T Ridge
Archive of Formal Proofs 2004, 2004
122004
TCP, UDP, and Sockets: Volume 3: The service-level specification
T Ridge, M Norrish, P Sewell
University of Cambridge, Computer Laboratory, 2009
102009
Operational reasoning for concurrent Caml programs and weak memory models
T Ridge
International Conference on Theorem Proving in Higher Order Logics, 278-293, 2007
102007
Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL
T Ridge
arXiv preprint cs/0607058, 2006
82006
A mechanically verified, efficient, sound and complete theorem prover for first order logic. Archive of Formal Proofs (2004)
T Ridge
72004
Completeness theorem
J Margetson, T Ridge
Archive of Formal Proofs. http://afp. sf. net/entries/Completeness. shtml, 2004
72004
Simple, efficient, sound-and-complete combinator parsing for all context-free grammars, using an oracle
T Ridge
SLE 2014, 2014
52014
The system can't perform the operation now. Try again later.
Articles 1–20