Tom Ridge

21 papers A* 3A 2B 5Journal 6Unranked 5
YearRankTypeTitle / Venue / Authors
2024 J jnl
Visualizing the Evaluation of Functional Programs for Debugging.
CoRR
John G. Whitington, Tom Ridge
2019 J jnl
Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API.
J. ACM
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough
2017 — conf
Direct Interpretation of Functional Programs for Debugging.
ML/OCaml
John G. Whitington, Tom Ridge
2017 — conf
Visualizing the Evaluation of Functional Programs for Debugging.
SLATE
John G. Whitington, Tom Ridge
2015 A* conf
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems.
SOSP
Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, Peter Sewell
2014 A conf
Lem: reusable engineering of real-world semantics.
ICFP
Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, Peter Sewell
2014 B conf
Simple, Efficient, Sound and Complete Combinator Parsing for All Context-Free Grammars, Using an Oracle.
SLE
Tom Ridge
2011 B conf
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars.
CPP
Tom Ridge
2011 B conf
The 1st Verified Software Competition: Experience Report.
FM
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß
2010 — conf
A Rely-Guarantee Proof System for x86-TSO.
VSTTE
Tom Ridge
2009 A* conf
The semantics of x86-CC multiprocessor machine code.
POPL
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave
2009 A* conf
Verifying distributed systems: the operational approach.
POPL
Tom Ridge
2008 B conf
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service.
FM
Tom Ridge, Michael Norrish, Peter Sewell
2007 — conf
Operational Reasoning for Concurrent Caml Programs and Weak Memory Models.
TPHOLs
Tom Ridge
2007 A conf
Ott: effective tool support for the working semanticist.
ICFP
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa
2006 J jnl
Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL
CoRR
Tom Ridge
2006 B conf
Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL.
ICNP
Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell
2005 — conf
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.
TPHOLs
Tom Ridge, James Margetson
2004 J jnl
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic.
Arch. Formal Proofs
Tom Ridge
2004 J jnl
Completeness theorem.
Arch. Formal Proofs
James Margetson, Tom Ridge
2004 J jnl
Ramsey's theorem, infinitary version.
Arch. Formal Proofs
Tom Ridge