 |
Dr Tom Ridge |
Introduction
I work on program verification, formal methods and theorem proving. In general, I am interested in what we can prove about the systems we can build, and what those proofs say about the systems we should build. My current focus is on
- reasoning directly with operational semantics (see publications)
- weak memory
- parsing
- (verified) filesystems
Past projects
- Previously I worked on the NetSem project, formalizing TCP/IP, at the Computer Laboratory, University of Cambridge.
Background
- I did my PhD at the Laboratory for the Foundations of Computer Science, University of Edinburgh. My supervisor was Paul Jackson.
- My undergraduate degree is in mathematics from Trinity College, University of Cambridge, where I also did the Diploma in Computer Science (somewhat similar to a Master's degree).
- I have a senior scholarship from Trinity College listed here, which I only found out about many years after it was awarded.
- After the diploma I spent a couple of years in the City of London. I was paid much more than I earn now, even though it was my first real job!
PhD and postdoc positions at Leicester
- I am very keen to supervise PhD students!
- Please contact me via email with a project proposal and a CV if you wish to pursue a PhD under my supervision.
- Current projects include: a verified filesystem; program verification on top of operational semantics.
- Fulbright scholarships for US citizens here
Teaching
 |
 |
Business
 | Giving world online |
 | VDomain/VDT |
Parsing
There is an introduction to the verified parsing work here.
Publications
- publications.bib
- DBLP
- google scholar
- blog The blog includes an RSS/Atom/email feed, and comment functionality... please comment!
Tom Ridge. Simple, functional, sound and complete parsing for all context-free grammars. In Jean Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 103--118. Springer, 2011. Keywords: verified, mechanized, formal, parsing, sound, complete, functional, combinator. paper and supporting material
Tom Ridge. Simple, functional, sound and complete parsing for all context-free grammars (unpublished draft). ridge10parsing.pdf
Vladimir Klebanov, Peter Muller, Natarajan Shankar, Gary T. Leavens, Valentin Wustholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiss. The 1st Verified Software Competition: Experience report. In Michael Butler and Wolfram Schulte, editors, Proceedings, 17th International Symposium on Formal Methods (FM 2011), 2011. Winner of the best paper prize! paper and additional material
Tom Ridge. A rely-guarantee proof system for x86-TSO. In Gary T. Leavens, Peter O'Hearn, and Sriram K. Rajamani, editors, VSTTE, volume 6217 of Lecture Notes in Computer Science, pages 55--70. Springer, 2010. ridge10vstte.pdf
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strni\v sa. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20(1):70--122, January 2010. ridge10ott-jfp.pdf
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. In Zhong Shao and Benjamin C. Pierce, editors, POPL, pages 379--391. ACM, 2009. popl09.pdf
Tom Ridge. Verifying distributed systems: the operational approach. In Zhong Shao and Benjamin C. Pierce, editors, POPL, pages 429--440. ACM, 2009. Keywords: verified, mechanized, formal, message, queue, OCaml. ridge09popl.pdf
Tom Ridge, Michael Norrish, and Peter Sewell. A rigorous approach to networking: TCP, from implementation to protocol to service. In Jorge Cuellar, T. S. E. Maibaum, and Kaisa Sere, editors, FM, volume 5014 of Lecture Notes in Computer Science, pages 294--309. Springer, 2008. ridge08stream-spec.pdf
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, and Rok Strnisa. Ott: effective tool support for the working semanticist. In Ralf Hinze and Norman Ramsey, editors, ICFP, pages 1--12. ACM, 2007. ott.pdf
Tom Ridge. To arrive where we started: experience of mechanizing binding. In Proceedings of the Workshop on Mechanizing Metatheory, October 2007. ridge07wmm.pdf
Tom Ridge. Operational reasoning for concurrent Caml programs and weak memory models. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, volume 4732 of Lecture Notes in Computer Science, pages 278--293. Springer, 2007. ridge07tphols.pdf
Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, and Peter Sewell. Rigorous protocol design in practice: An optical packet-switch MAC in HOL. In ICNP, pages 117--126. IEEE Computer Society, 2006. ridge06icnp.pdf
Tom Ridge and James Margetson. A mechanically verified, sound and complete theorem prover for FOL. In Joe Hurd and Tom Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, volume 3603 of Lecture Notes in Computer Science. Springer, August 2005. prover.pdf