James Brotherston

40 papers A* 7A 4B 13Journal 12Unranked 4

Year	Rank	Type	Title / 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