James Brotherston

Publication Activity (10 Years)

Years Active: 2001-2021
Publications (10 Years): 13

Top Topics

Deductive Reasoning

Classical Logic

Related Problems

Top Venues

Publications

James Brotherston, Paul Brunet, Nikos Gorogiannis, Max I. Kanovich
A Compositional Deadlock Detector for Android Java. ASE (2021)
Gadi Tellez, James Brotherston
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. J. Autom. Reason. 64 (3) (2020)
James Brotherston, Diana Costa, Aquinas Hobor, John Wickerson
Reasoning over Permissions Regions in Concurrent Separation Logic. CAV (2) (2020)
James Brotherston, Max I. Kanovich
On the Complexity of Pointer Arithmetic in Separation Logic. APLAS (2018)
James Brotherston, Max I. Kanovich
On the Complexity of Pointer Arithmetic in Separation Logic (an extended version). CoRR (2018)
Gadi Tellez, James Brotherston
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. CADE (2017)
Reuben N. S. Rowe, James Brotherston
Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent. TABLEAUX (2017)
James Brotherston, Nikos Gorogiannis, Max I. Kanovich
Biabduction (and Related Problems) in Array Separation Logic. CADE (2017)
Reuben N. S. Rowe, James Brotherston
Automatic cyclic termination proofs for recursive procedures in separation logic. CPP (2017)
Reuben N. S. Rowe, James Brotherston
Size Relationships in Abstract Cyclic Entailment Systems. CoRR (2017)
Jeremy E. Dawson, James Brotherston, Rajeev Goré
Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi. IJCAR (2016)
James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe
Model checking for symbolic-heap separation logic with inductive predicates. POPL (2016)
James Brotherston, Nikos Gorogiannis, Max I. Kanovich
Biabduction (and Related Problems) in Array Separation Logic. CoRR (2016)
James Brotherston, Nikos Gorogiannis
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation. TABLEAUX (2015)
James Brotherston, Jules Villard
Sub-classical Boolean Bunched Logics and the Meaning of Par. CSL (2015)
James Brotherston, Max I. Kanovich
Undecidability of Propositional Separation Logic and Its Neighbours. J. ACM 61 (2) (2014)
James Brotherston, Nikos Gorogiannis
Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. SAS (2014)
James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, Nikos Gorogiannis
A decision procedure for satisfiability in separation logic with inductive predicates. CSL-LICS (2014)
James Brotherston, Jules Villard
Parametric completeness for separation theories. POPL (2014)
James Brotherston, Nikos Gorogiannis, Rasmus Lerchedahl Petersen
A Generic Cyclic Theorem Prover. APLAS (2012)
James Brotherston
Bunched Logics Displayed. Stud Logica 100 (6) (2012)
James Brotherston, Alex Simpson
Sequent calculi for induction and infinite descent. J. Log. Comput. 21 (6) (2011)
James Brotherston, Rajeev Goré
Craig Interpolation in Displayable Logics. TABLEAUX (2011)
James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen
Automated Cyclic Entailment Proofs in Separation Logic. CADE (2011)
James Brotherston, Cristiano Calcagno
Classical BI: Its Semantics and Proof Theory Log. Methods Comput. Sci. 6 (3) (2010)
James Brotherston
A Unified Display Proof Theory for Bunched Logic. MFPS (2010)
James Brotherston, Max I. Kanovich
Undecidability of Propositional Separation Logic and Its Neighbours. LICS (2010)
James Brotherston, Cristiano Calcagno
Classical BI: a logic for reasoning about dualising resources. POPL (2009)
James Brotherston, Richard Bornat, Cristiano Calcagno
Cyclic proofs of program termination in separation logic. POPL (2008)
James Brotherston
Formalised Inductive Reasoning in the Logic of Bunched Implications. SAS (2007)
James Brotherston, Alex Simpson
Complete Sequent Calculi for Induction and Infinite Descent. LICS (2007)
James Brotherston
Cyclic Proofs for First-Order Logic with Inductive Definitions. TABLEAUX (2005)
René Vestergaard, James Brotherston
A formalised first-order confluence proof for the -calculus using one-sorted variable names. Inf. Comput. 183 (2) (2003)
James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa
Searching for Invariants Using Temporal Resolution. LPAR (2002)
René Vestergaard, James Brotherston
A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names. RTA (2001)
René Vestergaard, James Brotherston
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). Electron. Notes Theor. Comput. Sci. 58 (1) (2001)