Publications

James Brotherston (UCL):

J. Brotherston, N. Gorogiannis and M. Kanovich. Biabduction (and Related Problems) in Array Separation Logic. In Proceedings of CADE-26, 2017.

G. Tellez Espinosa and J. Brotherston. Automatically Verifying Temporal Properties of Programs with Cyclic Proof. In Proceedings of CADE-26, 2017.

R. Rowe and J. Brotherston. Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic. In Proceedings of CPP-6, 2017.

J. Brotherston, N. Gorogiannis, M. Kanovich and R. Rowe. Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates. In Proceedings of POPL-43, 2016.

J. Brotherston and N. Gorogiannis. Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. In Proceedings of SAS-21, 2014.

J. Brotherston, C. Fuhs, N. Gorogiannis and J. Navarro Perez. A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates. In Proceedings of CSL-LICS, 2014.

J. Brotherston and M. Kanovich. Undecidability of Propositional Separation Logic and its Neighbours. In Journal of the ACM 61(2), April 2014.

J. Brotherston and J. Villard. Parametric Completeness for Separation Theories. In Proceedings of POPL-41, 2014.

Alistair Donaldson (Imperial):

A. Betts, N. Chong, A. F. Donaldson, J. Ketema,
S. Qadeer, P. Thomson, and J. Wickerson. The design
and implementation of a verification technique for GPU
kernels. TOPLAS, 37(3):10, 2015. https://dl.acm.org/citation.cfm?doid=2743017

A. F. Donaldson, J. Ketema, T.Sorensen, J. Wickerson. Forward Progress on GPU Concurrency. 28th International Conference on Concurrency Theory, {CONCUR} 2017, p. 1:1–1:13.  https://doi.org/10.4230/LIPIcs.CONCUR.2017.1

T. Sorensen, H. Evrard and  Alastair F. Donaldson, Cooperative Kernels: GPU Multitasking for Blocking Algorithms.  Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, {ESEC/FSE} 2017, Paderborn, Germany, September 4-8, (2017),  p. 431–441. ttp://doi.acm.org/10.1145/3106237.3106265

David Pym (UCL):

G. Anderson and D. Pym. A Calculus and Logic of Bunched Resources and Processes. Theoretical Computer Science 614:63-96, 2016.
https://www.sciencedirect.com/science/article/pii/S0304397515011214

T. Caufield and D. Pym. Improving Security Policy Decisions with Models. IEEE Security and Privacy, 13(5), 34-41, Sept/Oct 2015.
http://www0.cs.ucl.ac.uk/staff/D.Pym/CP15a.pdf.
The Julia package used for creating system models may be obtained from GitHub: https://github.com/tristanc/SysModels

T. Caulfield and D. Pym. Modelling and Simulating Systems Security Policy. In Proc. SIMUTools 2015, ACM Digital Library: https://dl.acm.org/citation.cfm?id=2832181

G. Anderson and D. Pym. Substructural modal logic for optimal resource allocation. Paper 5, Proc. Strategic Reasoning 2015, St. Catharine’s College, Oxford, September 21-22, 2015.

G. Anderson and D. Pym. Trust Domains in system models: algebra, logic, utility, and combinators. J. of Logic & Computation 2015: doi: 10.1093/logcom/ exv030.

M. Collinson, B. Monahan, and D. Pym. A Disci- pline of Mathematical Systems Modelling. College Publications, 2012. https://www.amazon.co.uk/Discipline-Mathematical-Modelling-Thinking-Engineering/dp/1904987508/ref=sr_1_1?ie=UTF8&qid=1533205429&sr=81&keywords=A+Discipline+of+Mathematical+Systems+Modelling

M. Collinson and D. Pym. Algebra and Logic for Resource-based Systems Modelling. Mathematical Structures in Computer Science 19:959-1027, 2009.
doi:10.1017/S0960129509990077. http://www0.cs.ucl.ac.uk/staff/D.Pym/mbi.pdf

Edmund Robinson (QMUL):

C Hermida, US Reddy, EP Robinson. Logical relations and parametricity–a Reynolds programme for category theory and programming languages Electronic Notes in Theoretical Computer Science 303, 149-180. https://doi.org/10.1016/j.entcs.2014.02.008

COLLINSON, M., PYM, D., & ROBINSON, E. (2008). Bunched polymorphism. Mathematical Structures in Computer Science, 18(6), 1091-1132. https://doi:10.1017/S0960129508007159

EP Robinson, Variations on Algebra: Monadicity and Generalisations of Equational Theories Formal Aspects of Computing (2002) 13: 308  https://doi.org/10.1007/s001650200014

John Power and Edmund Robinson. 2000. Logical relations, data abstraction, and structured fibrations. In Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP ’00), Frank Pfenning (Ed.). ACM, New York, NY, USA, 15-23. D OI=http://dx.doi.org/10.1145/351268.351271