James Brotherston

40 papers A* 7A 4B 13Journal 12Unranked 4
YearRankTypeTitle / Venue / Authors
2025 B conf
Cyclic Proofs in Hoare Logic and its Reverse.
MFPS
James Brotherston, Quang Loc Le, Gauri Desai, Yukihiro Oda
2025 J jnl
The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions.
J. Log. Comput.
Yukihiro Oda, James Brotherston, Makoto Tatsuta
2024 J jnl
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations.
CoRR
Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson
2024 J jnl
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations.
Proc. ACM Program. Lang.
Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson
2021 A* conf
A Compositional Deadlock Detector for Android Java.
ASE
James Brotherston, Paul Brunet, Nikos Gorogiannis, Max I. Kanovich
2020 J jnl
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof.
J. Autom. Reason.
Gadi Tellez, James Brotherston
2020 — conf
Reasoning over Permissions Regions in Concurrent Separation Logic.
CAV (2)
James Brotherston, Diana Costa, Aquinas Hobor, John Wickerson
2018 J jnl
On the Complexity of Pointer Arithmetic in Separation Logic (an extended version).
CoRR
James Brotherston, Max I. Kanovich
2018 B conf
On the Complexity of Pointer Arithmetic in Separation Logic.
APLAS
James Brotherston, Max I. Kanovich
2017 B conf
Automatic cyclic termination proofs for recursive procedures in separation logic.
CPP
Reuben N. S. Rowe, James Brotherston
2017 A conf
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof.
CADE
Gadi Tellez, James Brotherston
2017 A conf
Biabduction (and Related Problems) in Array Separation Logic.
CADE
James Brotherston, Nikos Gorogiannis, Max I. Kanovich
2017 B conf
Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent.
TABLEAUX
Reuben N. S. Rowe, James Brotherston
2017 J jnl
Size Relationships in Abstract Cyclic Entailment Systems.
CoRR
Reuben N. S. Rowe, James Brotherston
2016 J jnl
Biabduction (and Related Problems) in Array Separation Logic.
CoRR
James Brotherston, Nikos Gorogiannis, Max I. Kanovich
2016 A conf
Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi.
IJCAR
Jeremy E. Dawson, James Brotherston, Rajeev Goré
2016 A* conf
Model checking for symbolic-heap separation logic with inductive predicates.
POPL
James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe
2015 B conf
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation.
TABLEAUX
James Brotherston, Nikos Gorogiannis
2015 B conf
Sub-classical Boolean Bunched Logics and the Meaning of Par.
CSL
James Brotherston, Jules Villard
2014 — conf
A decision procedure for satisfiability in separation logic with inductive predicates.
CSL-LICS
James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, Nikos Gorogiannis
2014 B conf
Cyclic Abduction of Inductively Defined Safety and Termination Preconditions.
SAS
James Brotherston, Nikos Gorogiannis
2014 A* conf
Parametric completeness for separation theories.
POPL
James Brotherston, Jules Villard
2014 J jnl
Undecidability of Propositional Separation Logic and Its Neighbours.
J. ACM
James Brotherston, Max I. Kanovich
2012 B conf
A Generic Cyclic Theorem Prover.
APLAS
James Brotherston, Nikos Gorogiannis, Rasmus Lerchedahl Petersen
2012 J jnl
Bunched Logics Displayed.
Stud Logica
James Brotherston
2011 A conf
Automated Cyclic Entailment Proofs in Separation Logic.
CADE
James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen
2011 B conf
Craig Interpolation in Displayable Logics.
TABLEAUX
James Brotherston, Rajeev Goré
2011 J jnl
Sequent calculi for induction and infinite descent.
J. Log. Comput.
James Brotherston, Alex Simpson
2010 B conf
A Unified Display Proof Theory for Bunched Logic.
MFPS
James Brotherston
2010 J jnl
Classical BI: Its Semantics and Proof Theory
Log. Methods Comput. Sci.
James Brotherston, Cristiano Calcagno
2010 A* conf
Undecidability of Propositional Separation Logic and Its Neighbours.
LICS
James Brotherston, Max I. Kanovich
2009 A* conf
Classical BI: a logic for reasoning about dualising resources.
POPL
James Brotherston, Cristiano Calcagno
2008 A* conf
Cyclic proofs of program termination in separation logic.
POPL
James Brotherston, Richard Bornat, Cristiano Calcagno
2007 A* conf
Complete Sequent Calculi for Induction and Infinite Descent.
LICS
James Brotherston, Alex Simpson
2007 B conf
Formalised Inductive Reasoning in the Logic of Bunched Implications.
SAS
James Brotherston
2005 B conf
Cyclic Proofs for First-Order Logic with Inductive Definitions.
TABLEAUX
James Brotherston
2003 J jnl
A formalised first-order confluence proof for the -calculus using one-sorted variable names.
Inf. Comput.
René Vestergaard, James Brotherston
2002 B conf
Searching for Invariants Using Temporal Resolution.
LPAR
James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa
2001 — conf
A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names.
RTA
René Vestergaard, James Brotherston
2001 — conf
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective).
MERLIN
René Vestergaard, James Brotherston