Browse by UCL people
Group by: Type | Date
Jump to: Article | Proceedings paper
Number of items: 16.
Article
Brotherston, J;
Kanovich, M;
(2014)
Undecidability of Propositional Separation Logic and Its Neighbours.
JOURNAL OF THE ACM
, 61
(2)
, Article ARTN 14. 10.1145/2542667.
|
 |
|
Oda, Yukihiro;
Brotherston, James;
Tatsuta, Makoto;
(2023)
The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions.
Journal of Logic and Computation
, Article exad068. 10.1093/logcom/exad068.
(In press).
|
|
Tellez, G;
Brotherston, J;
(2019)
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof.
Journal of Automated Reasoning
10.1007/s10817-019-09532-0.
(In press).
|
 |
Proceedings paper
|
Brotherston, J;
Brunet, P;
Gorogiannis, N;
Kanovich, M;
(2022)
A Compositional Deadlock Detector for Android Java.
In:
Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering.
Association for Computing Machinery (ACM)
(In press).
|
|
|
Brotherston, J;
Gorogiannis, N;
Petersen, RL;
(2012)
A generic cyclic theorem prover.
In:
Asian Symposium on Programming Languages and Systems APLAS 2012: Programming Languages and Systems.
(pp. pp. 350-367).
Springer: Berlin, Heidelberg.
|
|
|
Brotherston, J;
Costa, D;
Hobor, A;
Wickerson, J;
(2020)
Reasoning over Permissions Regions in Concurrent Separation Logic.
In:
Computer Aided Verification.
(pp. pp. 203-224).
Springer: Switzerland, Cham.
|
|
|
Brotherston, J;
Fuhs, C;
Pérez, JAN;
Gorogiannis, N;
(2014)
A decision procedure for satisfiability in separation logic with inductive predicates.
In:
Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014.
Association for Computing Machinery (ACM): New York, US.
|
|
|
Brotherston, J;
Gorogiannis, N;
(2015)
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation.
In:
Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings.
(pp. pp. 287-303).
Springer International Publishing: Switzerland.
|
|
Brotherston, J;
Gorogiannis, N;
(2014)
Cyclic abduction of inductively defined safety and termination preconditions.
In:
Cyclic Abduction of Inductively Defined Safety and Termination Precondition.
(pp. 68 - 84).
Springer International Publishing: Switzerland.
|
|
|
Brotherston, J;
Gorogiannis, N;
Kanovich, MI;
Rowe, R;
(2016)
Model checking for symbolic-heap separation logic with inductive predicates.
In: Bodik, R and Majumdar, R, (eds.)
(pp. pp. 84-96).
ACM
|
|
|
Brotherston, J;
Kanovich, M;
(2018)
On the Complexity of Pointer Arithmetic in Separation Logic.
In:
Programming Languages and Systems.
(pp. pp. 329-349).
Springer: Cham, Switzerland.
|
|
|
Brotherston, J;
Kanovich, M;
Gorogiannis, N;
(2017)
Biabduction (and related problems) in array separation logic.
In: De Moura, L, (ed.)
Automated Deduction – CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings.
(pp. pp. 472-490).
Springer: Cham, Switzerland.
|
|
|
Brotherston, J;
Villard, J;
(2015)
Sub-classical Boolean Bunched Logics and the Meaning of Par.
In: Kreutzer, S, (ed.)
(pp. pp. 325-342).
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
|
|
|
Rowe, RNS;
Brotherston, J;
(2017)
Automatic cyclic termination proofs for recursive procedures in separation logic.
In:
CPP 2017 Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs.
(pp. pp. 53-65).
Association for Computing Machinery: New York.
|
|
|
Rowe, RNS;
Brotherston, J;
(2017)
Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent.
In: Schmidt, RA and Nalon, C, (eds.)
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017).
(pp. pp. 295-310).
Springer: Cham, Switzerland.
|
|
|
Tellez, G;
Brotherston, J;
(2017)
Automatically verifying temporal properties of pointer programs with cyclic proof.
In: De Moura, L, (ed.)
Automated Deduction – CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings.
(pp. pp. 491-508).
Springer: Cham, Switzerland.
|
