Publications

James Brotherston (UCL):

James Brotherston, Paul Brunet, Nikos Gorogiannis and Max Kanovich. A Compositional Deadlock Detector for Android Java. To appear in Proceedings of ASE-36, 2021.

James Brotherston, Diana Costa, Aquinas Hobor and John Wickerson. Reasoning over Permissions Regions in Concurrent Separation Logic. In Proceedings of CAV-32, 2020.

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.

Paul Brunet (UCL):

On series-parallel pomset languages: Rationality, context-freeness and automata, Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi, in Journal of Logical and Algebraic Methods in Programming, Volume 103, February 2019, Pages 130-153.

A Kleene theorem for nominal automata, Paul Brunet and Alexandra Silva, in ICALP, 2019.

Kleene Algebra with Observations, Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi, in CONCUR 2019.

A Complete Axiomatisation of a Fragment of Language Algebra, Paul Brunet, in CSL, 2020.

Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness, Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi, to appear in FoSSaCS 2020

Diana Costa (UCL):

Diana Costa, Manuel A. Martins, “A Roadmap of Paraconsistent Hybrid Logics” in “Abstract Consequence and Logics: Essays in Honor of Edelcio G. de Souza”, Alexandre Costa-Leite, ed. (https://www.collegepublications.co.uk/tributes/?00042)

Diana Costa, Manuel A. Martins, João Marcos:
On Herbrand’s Theorem for Hybrid Logic. FLAP 6(2): 209-228 (2019)

Diana Costa, Manuel A. Martins:
A Four-Valued Hybrid Logic with Non-dual Modal Operators. DaLí 2019: 88-103

Tristan Caufield

T Caulfield, M.-C Ilau, and D Pym. Meta-modelling for ecosystems security. In Proc 13th SIMUtools 2021. Springer, 2021.

T Caulfield, M.-C Ilau, and D Pym. Engineering ecosystem models: semantics and pragmatics. In Proc. 13th SIMUtools 2021. Springer, 2021.

A. Baldwin, T. Caulfield, M.-C. Ilau, and D. Pym. Modelling Organizational Recovery. In Proc. 13th SIMUtools 2021. Springer, 2021.

Alastair Donaldson (Imperial):

Lascu, A., Donaldson, A.F., Grosser, T., & Hoefler, T. (2022). Metamorphic Fuzzing of C++ Libraries. 2022 IEEE Conference on Software Testing, Verification and Validation (ICST), 35-46.

CsmithEdge: More Effective Compiler Testing by Handling Undefined Behaviour Less Conservatively. Karine Even-Mendoza, Cristian Cadar, Alastair F. Donaldson. Journal of Empirical Software Engineering, 2022.

Andrei Lascu, Matt Windsor, Alastair F. Donaldson, Tobias Grosser, John Wickerson:Dreaming up Metamorphic Relations: Experiences from Three Fuzzer Tools. MET@ICSE 2021: 61-68

High-coverage Metamorphic Testing of Concurrency Support in C Compilers. Matt Windsor, Alastair F. Donaldson, John Wickerson. Journal of Software: Testing, Verification and Reliability, 2022.

Combining Static Analysis Error Traces with Dynamic Symbolic Execution (Experience Paper). Frank Busse, Pritam Gharat, Cristian Cadar, Alastair F. Donaldson

Matt Windsor, Alastair F. Donaldson, John Wickerson: C4: the C compiler concurrency checker. ISSTA 2021: 670-67

Alastair F. Donaldson, Paul Thomson, Vasyl Teliman, Stefano Milizia, André Perez Maselco, Antoni Karpinski:Test-case reduction and deduplication almost for free with transformation-based compiler testing. PLDI 2021: 1017-1032

Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, Alastair F. Donaldson:Specifying and Testing GPU Workgroup Progress Models. CoRR abs/2109.06132 (2021)

A. Betts, N. Chong, A. F. Donaldson, J. Ketema,S. Qadeer, P. Thomson, and J. Wickerson. The designand 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

Christopher Lidbury and Alastair F.Donaldson.2019.Sparse Record and Replay with Controlled Scheduling. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’19), June 22–26, 2019, Phoenix, AZ, USA. ACM, New York, NY,USA, 18 pages. https://doi.org/10.1145/3314221. 3314635

Lê Quang Lộc

Finding Real Bugs in Big Programs with Incorrectness Logic. Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. Proc. ACM Program. Lang. 6 (OOPSLA 2022)

REFIXAR: Multi-version Reasoning for Automated Repair of Regression Errors. D.-X. Bach Le, Quang Loc Le. The 32nd International Symposium on Software Reliability Engineering (ISSRE’21)

Peter O’Hearn (Facebook)

Peter W. O’Hearn:
Incorrectness logic. PACMPL 4(POPL): 10:1-10:32 (2020)

Peter W. O’Hearn:
Separation logic. Commun. ACM 62(2): 86-95 (2019)

Dino Distefano, Manuel Fähndrich, Francesco Logozzo, Peter W. O’Hearn:
Scaling static analyses at Facebook. Commun. ACM 62(8): 62-70 (2019)

Nikos Gorogiannis, Peter W. O’Hearn, Ilya Sergey:
A true positives theorem for a static race detector. PACMPL 3(POPL): 57:1-57:29 (2019)

Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, Ilya Sergey:
RacerD: compositional static race detection. PACMPL 2(OOPSLA): 144:1-144:28 (2018)

Roser Pujadas (LSE):

Publications and conference proceedings

Pujadas, R., Valderrama, E., Venters, W. (2020) Interfaces and the Dynamics of Digital Ecosystems: A Study of the Online Travel Ecosystem, Proceedings of the 41st International Conference on Information Systems (ICIS), India 2020

Pujadas, R, Thompson, M., Venters, W., Wardley, S. (2019) Building situational awareness in the age of service ecosystems. In Proceedings of the 27th European Conference on Information Systems (ECIS), Stockholm & Uppsala, Sweden, June 8-14, 2019. ISBN 978-1-7336325-0-8 Research Papers.
https://aisel.aisnet.org/ecis2019_rp/178/

Pujadas, R. and Curto-Millet, D. (2019), “From Matchmaking to Boundary Making: Thinking Infrastructures and Decentring Digital Platforms in the Sharing Economy”, Kornberger, M., Bowker, G., Elyachar, J., Mennicken, A., Miller, P., Nucho, J. and Pollock, N. (Eds.) Thinking Infrastructures (Research in the Sociology of Organizations, Vol. 62), Emerald Publishing Limited, pp. 273-286. https://www.emerald.com/insight/content/doi/10.1108/S0733-558X20190000062017/full/html

Presentations in conferences and research seminars

Pujadas, R., Valderrama, E. (2020) Digital interfacing and the dynamics of digital ecosystems: Lessons from an online travel ecosystem (Conference for the Special Issue of Research Policy: “Innovation Ecosystems and Ecosystem Innovation”, Copenhagen, June 2020

Slavova, M., Pujadas, R. (2020) Making contact in rural Africa: A study of connectivity practices of Ghanaian agricultural agents (PROS conference, June 2020 –paper accepted, but conference cancelled due to COVID19)

Pujadas, R., Thompson, M., Venters, W (2019) Situational awareness in digital ecosystems: mapping and sensemaking. INDEX research community meeting, University of Exeter, INDEX, London, October 2019.

Pujadas, R, Thompson, M., Venters, W.(2019) Situational awareness in digital ecosystems: Mapping in strategizing. In Strategy-as-Practice (SAP) Community Day: Rethinking Strategy Research in the Digital Age, EGOS 2019 Pre-Colloquium workshop, Edinburgh, July 2019.

Gueddana, W. & Pujadas, R. (2019) “Labour and platform work in the ‘sharing economy’”. EGOS 2019 Colloquium, Edinburgh, July 2019.

Gueddana,W., Pujadas,R. (2019) Studying the Digital Recomposition of Labour: A Research Agenda. SASE, June 2019

David Pym (UCL):

David Pym, Eike Ritter, and Edmund Robinson. Proof-theoretic Semantics in Sheaves (Extended Abstract). Scandinavian Logic Symposium, Bergen, June 2022. Manuscript.

T. Caulfield, M.-C. Ilau, and D. Pym. Engineering Ecosystem Models: Semantics and Pragmatics. To
appear, Proc. 13th SIMUtools

A. Demjaha, T. Caulfield, and D. Pym. Found in Translation: Co-design for Security Modelling. To appear, Proc. STAST 2021.

T. Caulfield, M.-C. Ilau, and D. Pym. Metamodelling for Ecosystems Security. In Proc. 13th SIMUtools 2021. Springer, 2021. Manuscript.Springer Link

A. Demjaha, S. Parkin, and D. Pym. The bounded rational employee: Security economics for behaviour intervention support in organizations. In revision, Journal of Computer Security, 2021.

Diana Costa, James Brotherston, and David Pym. Graph Decomposition and Local Reasoning. Submitted 2021. Manuscript.

David Pym and Will Venters. Modelling interfaces in the decentralized Internet of Things. Submitted, 2020. Manuscript.

Paul Brunet and David Pym. Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra. FSCD 2020 version and arXiv version.

Didier Galmiche, Pierre Kimmel, and David Pym. A Substructural Epistemic Resource Logic: Theory and Modelling Applications. Journal of Logic and Computation, 29(8), 1251-1287, 2019. doi.org/10.1093/logcom/exz024. Published: 19 January 2020. Manuscript.

David Pym. Resource semantics: logic as a modelling technology. ACM SIGLOG News, April 2019, Vol. 6, No. 2, 5-41. Manuscript.

David Pym. Reductive logic & proof-theoretic semantics: a coalgebraic perspective. To appear: Proc. Proof-theoreti

Albese Demjaha, Tristan Caulfield, M. Angela Sasse, and David Pym. Fast 2 Secure: A Case Studyof Post-Breach Security Changes. In: Proc. 4th European Workshop on Usable Security, EuroUSEC2019, IEEE 2019. Stockholm, Sweden, June 20,2019. To appear: IEEE Xplore. Manuscript.

J.M. Spring, T. Moore, and D. Pym. Practicing a
Science of Security: A Philosophy of Science Perspective. To appear: Proc. New Security Paradigms Workshop, Islamorada, FL, USA, 2-4 Oct., 2017.doi: 10.475/xxx x. Manuscript.

T. Caulfield, C. Ioannidis, and D. Pym. The U.S.Vulnerabilities Equities Process: An Economic Perspective. Proc. GameSec 2017, LNCS 10575:131–
150, 2017, 2017. Manuscript.

T. Caulfield, C. Ioannidis, and D. Pym. On the adoption of privacy-enhancing technologies. Proc.GameSec 2016, LNCS 9996:175-194, 2016. M

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.

Edmund Robinson (QMUL):

Hermida, C., Reddy, U.S. and Robinson, E.P., 2019. Deriving Logical Relations from Interpretations of Predicate Logic. Electronic Notes in Theoretical Computer Science, 347, pp.241-259.

Hermida, C., Reddy, U., Robinson, E. and Santamaria, A., 2020. Bisimulation as a Logical Relation. arXiv preprint arXiv:2003.13542.

Lewis-Smith, A., Oliva, P. & Robinson, E. Kripke Semantics for Intuitionistic Łukasiewicz Logic. Stud Logica (2020). https://doi.org/10.1007/s11225-020-09908-z

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

Enrico Rossi

Lima, G. and Rossi, E (2022 or forthcoming) ‘Distributed ledger technology and the evolution of post-trade’, Journal of Securities Operations & Custody, 14(3): 1-35

Will Venters (LSE):

Publications and conference proceedings

Rossi, E., Pujadas, R, Venters, W. (2021) Epistemic Mirroring: how firms’ governance of internal relations shapes the interpretation of a digital ecosystem architecture. Proceedings of the UKAIS Conference.

Pym, M., Venters, W. (2020) Modelling Interfaces and Things Within the Decentralized Ecosystems of the Internet of Things, Proceedings of the 41st International Conference on Information Systems (ICIS), India 2020

Pujadas, R, Thompson, M., Venters, W., Wardley, S. (2019) Building situational awareness in the age of service ecosystems. 27th European Conference on Information Systems, Stockholm & Uppsala, June 2019.

Presentations in conferences and research seminars

Pujadas, R., Thompson, M., Venters, W (2019) Situational awareness in digital ecosystems: mapping and sensemaking. INDEX research community meeting, University of Exeter, INDEX, London, October 2019.

Pujadas, R., Thompson, M., Venters, W (2019) Situational awareness in digital ecosystems: mapping in strategizing. Strategy-as-Practice Pre-EGOS Workshop, July 2019.

Papers submitted pending review

Jones, M., Thompson, M., Venters, W. Shaping and Configuring: Digital capabilities and organizing vision in the practice of platform innovation, Information Systems Research.

Polyviou, A., Pouloudi,N., Venters, W. The Sensemaking Process and the Role of Proximity in Organizational Cloud Computing Adoption, Journal of Information Technology

John Wickerson:

Matt Windsor, Alastair F. Donaldson, and John Wickerson. C4: the C compiler concurrency checker. In ACM SIGSOFT Int. Symp. on Software Testing and Analysis, 2021. Tool demonstrations track.

Yann Herklotz, Zewei Du, Nadesh Ramanathan, and John Wickerson. An empirical study of the reliability of high-level synthesis tools. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2021. Short paper category.

Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, and John Wickerson. The semantics of shared memory in Intel CPU/FPGA systems. In ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, 2021.

Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal verification of high-level synthesis. In ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, 2021. Link:

Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, and Alastair F. Donaldson. Specifying and testing GPU workgroup progress models. In ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, 2021.

Nadesh Ramanathan, George A. Constantinides, and John Wickerson. Precise pointer analysis in high-level synthesis. In Int. Conf. on Field Programmable Logic and Applications, 2020.

James Brotherston, Diana Costa, Aquinas Hobor, and John Wickerson. Reasoning over permissions regions in concurrent separation logic. In Int. Conf. on Computer Aided Verification, 2020.

Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. Persistency semantics of the Intel-x86 architecture. In ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, 2020.

Patrick Sittel, John Wickerson, Martin Kumm, and Peter Zipf. Modulo scheduling with rational initiation intervals in custom hardware design. In Asia and South Pacific Design Automation Conference, 2020.

A. Raad, J. Wickerson, and V. Vafeiadis. Weak Persistency Semantics from the Ground Up. In Proceedings of the ACM on Programming Languages (OOPSLA), 2019.

P. Sittel, J. Wickerson, M. Kumm, and P. Zipf. Modulo scheduling with rational initiation intervals in custom hardware design. In Asia and South Pacific Design Automation Conference (ASP-DAC), 2020.

J. Cheng, L. Josipović, G. A. Constantinides, P. Ienne, and J. Wickerson. Combining Dynamic and Static Scheduling in High-Level Synthesis. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays (FPGA), 2020.

Y. Herklotz and J. Wickerson. Finding and understanding bugs in FPGA synthesis tools. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays (FPGA), 2020.

Dan Iorga, Tyler Sorensen, John Wickerson, and Alastair F. Donaldson. Slow and steady: Measuring and tuning multicore interference. In IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), 2020.