| 2020 | TACAS | Describing and Simulating Concurrent Quantum Systems. | Richard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly, Rajagopal Nagarajan |
| 2009 | VMCAI | Towards Automatic Stability Analysis for Rely-Guarantee Proofs. | Hasan Amjad, Richard Bornat |
| 2008 | CADE | Model Checking for Stability Analysis in Rely-Guarantee Proofs. | Hasan Amjad, Richard Bornat |
| 2008 | POPL | Cyclic proofs of program termination in separation logic. | James Brotherston, Richard Bornat, Cristiano Calcagno |
| 2007 | POPL | Modular verification of a non-blocking stack. | Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn |
| 2006 | LICS | Variables as Resource in Hoare Logics. | Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno |
| 2005 | POPL | Permission accounting in separation logic. | Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson |
| 2000 | MPC | Proving Pointer Programs in Hoare Logic. | Richard Bornat |
| 1997 | CADE | Jape: A Calculator for Animating Proof-on-Paper. | Richard Bornat, Bernard Sufrin |
| 1976 | ECAI | Reasoning about Hand Prinited FORTRAN Programs. | Richard Bornat |
| 1976 | ECAI | Finding Blobs of Writing in the FORTRAN Coding-Sheets Project. | Richard Bornat, J. Michael Brady |
| 1976 | ECAI | Does AI Programming really have to be like knitting with Spaghetti? | Richard Bornat, Bob J. Wielinga |