Follow
Tom Ridge
Title
Cited by
Cited by
Year
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
2072009
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
2042010
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
1322007
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
1172014
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
772011
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
752015
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
672005
A rely-guarantee proof system for x86-TSO
T Ridge
Verified Software: Theories, Tools, Experiments: Third International …, 2010
542010
Simple, functional, sound and complete parsing for all context-free grammars
T Ridge
Certified Programs and Proofs, 2011, 2011
402011
Verifying distributed systems: the operational approach
T Ridge
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2009
222009
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
222008
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
202018
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
132004
TCP, UDP, and Sockets: Volume 3: The Service-level Specification
T Ridge, M Norrish, P Sewell
University of Cambridge, Computer Laboratory, 2009
112009
Operational reasoning for concurrent Caml programs and weak memory models
T Ridge
International Conference on Theorem Proving in Higher Order Logics, 278-293, 2007
112007
Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL
T Ridge
arXiv preprint cs/0607058, 2006
92006
Completeness theorem
J Margetson, T Ridge
Archive of Formal Proofs. http://afp. sf. net/entries/Completeness. shtml, 2004
92004
A mechanically verified, efficient, sound and complete theorem prover for first order logic. Archive of Formal Proofs (2004)
T Ridge
92004
Simple, efficient, sound-and-complete combinator parsing for all context-free grammars, using an oracle
T Ridge
SLE 2014, 2014
82014
The system can't perform the operation now. Try again later.
Articles 1–20