| 2020 | CAV | Reasoning over Permissions Regions in Concurrent Separation Logic. | James Brotherston, Diana Costa, Aquinas Hobor, John Wickerson |
| 2018 | APLAS | On the Complexity of Pointer Arithmetic in Separation Logic. | James Brotherston, Max I. Kanovich |
| 2017 | CADE | Biabduction (and Related Problems) in Array Separation Logic. | James Brotherston, Nikos Gorogiannis, Max I. Kanovich |
| 2017 | CADE | Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. | Gadi Tellez, James Brotherston |
| 2017 | CPP | Automatic cyclic termination proofs for recursive procedures in separation logic. | Reuben N. S. Rowe, James Brotherston |
| 2017 | TABLEAUX | Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent. | Reuben N. S. Rowe, James Brotherston |
| 2016 | CADE | Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi. | Jeremy E. Dawson, James Brotherston, Rajeev Gor |
| 2016 | POPL | Model checking for symbolic-heap separation logic with inductive predicates. | James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe |
| 2015 | CSL | Sub-classical Boolean Bunched Logics and the Meaning of Par. | James Brotherston, Jules Villard |
| 2015 | TABLEAUX | Disproving Inductive Entailments in Separation Logic via Base Pair Approximation. | James Brotherston, Nikos Gorogiannis |
| 2014 | CSL | A decision procedure for satisfiability in separation logic with inductive predicates. | James Brotherston, Carsten Fuhs, Juan Antonio Navarro Prez, Nikos Gorogiannis |
| 2014 | POPL | Parametric completeness for separation theories. | James Brotherston, Jules Villard |
| 2014 | SAS | Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. | James Brotherston, Nikos Gorogiannis |
| 2012 | APLAS | A Generic Cyclic Theorem Prover. | James Brotherston, Nikos Gorogiannis, Rasmus Lerchedahl Petersen |
| 2011 | CADE | Automated Cyclic Entailment Proofs in Separation Logic. | James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen |
| 2011 | TABLEAUX | Craig Interpolation in Displayable Logics. | James Brotherston, Rajeev Gor |
| 2010 | LICS | Undecidability of Propositional Separation Logic and Its Neighbours. | James Brotherston, Max I. Kanovich |
| 2009 | POPL | Classical BI: a logic for reasoning about dualising resources. | James Brotherston, Cristiano Calcagno |
| 2008 | POPL | Cyclic proofs of program termination in separation logic. | James Brotherston, Richard Bornat, Cristiano Calcagno |
| 2007 | LICS | Complete Sequent Calculi for Induction and Infinite Descent. | James Brotherston, Alex Simpson |
| 2007 | SAS | Formalised Inductive Reasoning in the Logic of Bunched Implications. | James Brotherston |
| 2005 | TABLEAUX | Cyclic Proofs for First-Order Logic with Inductive Definitions. | James Brotherston |
| 2002 | LPAR | Searching for Invariants Using Temporal Resolution. | James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa |