Dr Tom Ridge

	computer science
	HOME	MAP	CONTACT

ABOUT

Back to staff listing

STAFF — Dr Tom Ridge

Lecturer

Computer Science Building
Department of Computer Science,
University of Leicester,
University Road,
Leicester,
LE1 7RH.

E: tr61@le.ac.uk

Dr Tom Ridge
Lecturer
F4, Department of Computer Science
University of Leicester
Leicester, LE1 7RH
0116 223 1304
tr61 (at) le.ac.uk

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

Past projects

Previously I worked on the NetSem project, formalizing TCP/IP, at the Computer Laboratory, University of Cambridge.

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

Publications

publications.bib
DBLP
google scholar
blog

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

\| \|\|\|\|\|\|\|\|
Author: Dr Tom Ridge (tr61@le.ac.uk). © University of Leicester Fri Jan 27 07:54:33 GMT 2012. Last modified: 27th January 2012, 07:54:33. CS Web Maintainer. Any opinions expressed on this page are those of the author.

computer science