default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJames Brotherston
Person information
SPARQL queries 
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j7]Luke Geeson
, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson:
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations. Proc. ACM Program. Lang. 8(OOPSLA2): 442-467 (2024)- [i4]Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson:
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations. CoRR abs/2409.01161 (2024) - 2021
- [c27]James Brotherston, Paul Brunet, Nikos Gorogiannis, Max I. Kanovich:
A Compositional Deadlock Detector for Android Java. ASE 2021: 955-966 - 2020
- [j6]Gadi Tellez, James Brotherston:
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. J. Autom. Reason. 64(3): 555-578 (2020) - [c26]James Brotherston, Diana Costa, Aquinas Hobor, John Wickerson:
Reasoning over Permissions Regions in Concurrent Separation Logic. CAV (2) 2020: 203-224
2010 – 2019
- 2018
- [c25]James Brotherston, Max I. Kanovich:
On the Complexity of Pointer Arithmetic in Separation Logic. APLAS 2018: 329-349 - [i3]James Brotherston, Max I. Kanovich:
On the Complexity of Pointer Arithmetic in Separation Logic (an extended version). CoRR abs/1803.03164 (2018) - 2017
- [c24]James Brotherston, Nikos Gorogiannis, Max I. Kanovich:
Biabduction (and Related Problems) in Array Separation Logic. CADE 2017: 472-490 - [c23]Gadi Tellez, James Brotherston:
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. CADE 2017: 491-508 - [c22]Reuben N. S. Rowe, James Brotherston:
Automatic cyclic termination proofs for recursive procedures in separation logic. CPP 2017: 53-65 - [c21]Reuben N. S. Rowe, James Brotherston:
Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent. TABLEAUX 2017: 295-310 - [i2]Reuben N. S. Rowe, James Brotherston:
Size Relationships in Abstract Cyclic Entailment Systems. CoRR abs/1702.03981 (2017) - 2016
- [c20]Jeremy E. Dawson, James Brotherston, Rajeev Goré:
Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi. IJCAR 2016: 452-468 - [c19]James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe:
Model checking for symbolic-heap separation logic with inductive predicates. POPL 2016: 84-96 - [i1]James Brotherston, Nikos Gorogiannis, Max I. Kanovich:
Biabduction (and Related Problems) in Array Separation Logic. CoRR abs/1607.01993 (2016) - 2015
- [c18]James Brotherston, Jules Villard:
Sub-classical Boolean Bunched Logics and the Meaning of Par. CSL 2015: 325-342 - [c17]James Brotherston, Nikos Gorogiannis:
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation. TABLEAUX 2015: 287-303 - 2014
- [j5]James Brotherston, Max I. Kanovich:
Undecidability of Propositional Separation Logic and Its Neighbours. J. ACM 61(2): 14:1-14:43 (2014) - [c16]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: 25:1-25:10 - [c15]James Brotherston, Jules Villard:
Parametric completeness for separation theories. POPL 2014: 453-464 - [c14]James Brotherston, Nikos Gorogiannis:
Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. SAS 2014: 68-84 - 2012
- [j4]James Brotherston:
Bunched Logics Displayed. Stud Logica 100(6): 1223-1254 (2012) - [c13]James Brotherston, Nikos Gorogiannis, Rasmus Lerchedahl Petersen:
A Generic Cyclic Theorem Prover. APLAS 2012: 350-367 - 2011
- [j3]James Brotherston, Alex Simpson:
Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6): 1177-1216 (2011) - [c12]James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen:
Automated Cyclic Entailment Proofs in Separation Logic. CADE 2011: 131-146 - [c11]James Brotherston, Rajeev Goré:
Craig Interpolation in Displayable Logics. TABLEAUX 2011: 88-103 - 2010
- [j2]James Brotherston, Cristiano Calcagno:
Classical BI: Its Semantics and Proof Theory. Log. Methods Comput. Sci. 6(3) (2010) - [c10]James Brotherston, Max I. Kanovich:
Undecidability of Propositional Separation Logic and Its Neighbours. LICS 2010: 130-139 - [c9]James Brotherston:
A Unified Display Proof Theory for Bunched Logic. MFPS 2010: 197-211
2000 – 2009
- 2009
- [c8]James Brotherston, Cristiano Calcagno:
Classical BI: a logic for reasoning about dualising resources. POPL 2009: 328-339 - 2008
- [c7]James Brotherston, Richard Bornat, Cristiano Calcagno:
Cyclic proofs of program termination in separation logic. POPL 2008: 101-112 - 2007
- [c6]James Brotherston, Alex Simpson:
Complete Sequent Calculi for Induction and Infinite Descent. LICS 2007: 51-62 - [c5]James Brotherston:
Formalised Inductive Reasoning in the Logic of Bunched Implications. SAS 2007: 87-103 - 2005
- [c4]James Brotherston:
Cyclic Proofs for First-Order Logic with Inductive Definitions. TABLEAUX 2005: 78-92 - 2003
- [j1]René Vestergaard, James Brotherston:
A formalised first-order confluence proof for the -calculus using one-sorted variable names. Inf. Comput. 183(2): 212-244 (2003) - 2002
- [c3]James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa:
Searching for Invariants Using Temporal Resolution. LPAR 2002: 86-101 - 2001
- [c2]René Vestergaard, James Brotherston:
A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names. RTA 2001: 306-321 - [c1]René Vestergaard, James Brotherston:
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). MERLIN 2001: 18-36
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-03-04 21:14 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
