James Brotherston

According to our database, James Brotherston authored at least 34 papers between 2001 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations.

Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson

Proc. ACM Program. Lang., 2024

2021

A Compositional Deadlock Detector for Android Java.

James Brotherston, Paul Brunet, Nikos Gorogiannis, Max I. Kanovich

Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering, 2021

2020

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof.

Gadi Tellez, James Brotherston

J. Autom. Reason., 2020

Reasoning over Permissions Regions in Concurrent Separation Logic.

James Brotherston, Diana Costa, Aquinas Hobor, John Wickerson

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2018

On the Complexity of Pointer Arithmetic in Separation Logic (an extended version).

James Brotherston, Max I. Kanovich

CoRR, 2018

On the Complexity of Pointer Arithmetic in Separation Logic.

James Brotherston, Max I. Kanovich

Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017

Size Relationships in Abstract Cyclic Entailment Systems.

Reuben N. S. Rowe, James Brotherston

CoRR, 2017

Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent.

Reuben N. S. Rowe, James Brotherston

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2017

Automatic cyclic termination proofs for recursive procedures in separation logic.

Reuben N. S. Rowe, James Brotherston

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

Biabduction (and Related Problems) in Array Separation Logic.

James Brotherston, Nikos Gorogiannis, Max I. Kanovich

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Model checking for symbolic-heap separation logic with inductive predicates.

James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi.

Jeremy E. Dawson, James Brotherston, Rajeev Goré

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Disproving Inductive Entailments in Separation Logic via Base Pair Approximation.

James Brotherston, Nikos Gorogiannis

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Sub-classical Boolean Bunched Logics and the Meaning of Par.

James Brotherston, Jules Villard

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

Undecidability of Propositional Separation Logic and Its Neighbours.

James Brotherston, Max I. Kanovich

J. ACM, 2014

Cyclic Abduction of Inductively Defined Safety and Termination Preconditions.

James Brotherston, Nikos Gorogiannis

Proceedings of the Static Analysis - 21st International Symposium, 2014

Parametric completeness for separation theories.

James Brotherston, Jules Villard

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

A decision procedure for satisfiability in separation logic with inductive predicates.

James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, Nikos Gorogiannis

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2012

Bunched Logics Displayed.

James Brotherston

Stud Logica, 2012

A Generic Cyclic Theorem Prover.

James Brotherston, Nikos Gorogiannis, Rasmus Lerchedahl Petersen

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Sequent calculi for induction and infinite descent.

James Brotherston, Alex Simpson

J. Log. Comput., 2011

Craig Interpolation in Displayable Logics.

James Brotherston, Rajeev Goré

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

Automated Cyclic Entailment Proofs in Separation Logic.

James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

A Unified Display Proof Theory for Bunched Logic.

James Brotherston

Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, 2010

Classical BI: Its Semantics and Proof Theory

James Brotherston, Cristiano Calcagno

Log. Methods Comput. Sci., 2010

2009

Classical BI: a logic for reasoning about dualising resources.

James Brotherston, Cristiano Calcagno

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

2008

Cyclic proofs of program termination in separation logic.

James Brotherston, Richard Bornat, Cristiano Calcagno

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

2007

Formalised Inductive Reasoning in the Logic of Bunched Implications.

James Brotherston

Proceedings of the Static Analysis, 14th International Symposium, 2007

Complete Sequent Calculi for Induction and Infinite Descent.

James Brotherston, Alex Simpson

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2005

Cyclic Proofs for First-Order Logic with Inductive Definitions.

James Brotherston

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2005

2003

A formalised first-order confluence proof for the -calculus using one-sorted variable names.

René Vestergaard, James Brotherston

Inf. Comput., 2003

2002

Searching for Invariants Using Temporal Resolution.

James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa

Proceedings of the Logic for Programming, 2002

2001

The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective).

René Vestergaard, James Brotherston

Proceedings of the Mechanized Reasoning about Languages with Variable Binding, 2001

A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names.

René Vestergaard, James Brotherston

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001