Interface reasoning for interacting systems (IRIS).
Lead Research Organisation:
University College London
Department Name: Computer Science
Abstract
The smooth functioning of society is critically dependent not only on the correctness of programs, particularly of programs controlling critical and high-sensitivity core components of individual systems, but also upon correct and robust interaction between diverse information-processing ecosystems of large, complex, dynamic, highly distributed systems. Failures are common, unpredictable, highly disruptive, and span multiple organizations.
The scale of systems' interdependence will increase by orders of magnitude in the next few years. Indeed by 2020, with developments in Cloud, the Internet of Things, and Big Data, we may be faced with a world of 25 million apps, 31 billion connected devices, 1.3 trillion tags/sensors, and a data store of 50 trillion gigabytes (data: IDC, ICT Outlook: Recovering Into a New World, #DR2010_GS2_JG, March 2010). Robust interaction between systems will be critical to everyone and
every aspect of society. Although the correctness and security of complete systems in this world cannot be verified, we can hope to be able to ensure that specific systems, such as verified safety-, security-, or identity-critical modules, are correctly interfaced.
The recent success of program verification notwithstanding, there remains little prospect of verifying such ecosystems in their entireties: the scale and complexity are just too great, as are the social and managerial coordination challenges. Even being able to define what it means to verify something that is going to have an undetermined role in a larger system presents a serious challenge. It is perhaps evident that the most critical aspect of the operation of these
information-processing ecosystems lies in their interaction: even perfectly specified and implemented individual systems may be used in contexts for which they were not intended, leading to unreliable, insecure communications between them.
We contend that interfaces supporting such interactions are therefore the critical mechanism for ensuring systems behave as intended. However, the verification/modelling techniques that have been so effective in ensuring reliability of low-level features of programs, protocols, and policies (and so the of the software that drives large systems) are, essentially, not applied to reasoning about such large-scale systems and their interfaces. We intend to explore this deficiency by researching
the technical, organizational, and social challenges of specifying and verifying interfaces in system ecosystems. In so doing, we will drive the use of verification techniques and improve the reliability of large systems.
Complex systems ecosystems and their interfaces are some of the most intricate and critical information ecosystems in existence today, and are highly dynamic and constantly evolving. We aim to understand how the interfaces between the components constituting these ecosystems work, and to verify them against their intended use. This research will be
undertaken through a collection of different themes covering systems topics where interface is crucially important, including critical code, communications and security protocols, distributed systems and networks, security policies, business ecosystems, and even extending to the physical architecture of buildings and networks. These themes are representative of the problem of specifying and reasoning about the correctness of interfaces at different levels of abstraction and criticality.
Interfaces of each degree of abstraction and criticality can be studied independently, but we believe that it will be possible to develop a quite general, uniform account of specifying and reasoning about them. It is unlikely that any one level of abstraction will suggest all of the answers: we expect that the work of the themes will evolve and interact
in complex ways.
The scale of systems' interdependence will increase by orders of magnitude in the next few years. Indeed by 2020, with developments in Cloud, the Internet of Things, and Big Data, we may be faced with a world of 25 million apps, 31 billion connected devices, 1.3 trillion tags/sensors, and a data store of 50 trillion gigabytes (data: IDC, ICT Outlook: Recovering Into a New World, #DR2010_GS2_JG, March 2010). Robust interaction between systems will be critical to everyone and
every aspect of society. Although the correctness and security of complete systems in this world cannot be verified, we can hope to be able to ensure that specific systems, such as verified safety-, security-, or identity-critical modules, are correctly interfaced.
The recent success of program verification notwithstanding, there remains little prospect of verifying such ecosystems in their entireties: the scale and complexity are just too great, as are the social and managerial coordination challenges. Even being able to define what it means to verify something that is going to have an undetermined role in a larger system presents a serious challenge. It is perhaps evident that the most critical aspect of the operation of these
information-processing ecosystems lies in their interaction: even perfectly specified and implemented individual systems may be used in contexts for which they were not intended, leading to unreliable, insecure communications between them.
We contend that interfaces supporting such interactions are therefore the critical mechanism for ensuring systems behave as intended. However, the verification/modelling techniques that have been so effective in ensuring reliability of low-level features of programs, protocols, and policies (and so the of the software that drives large systems) are, essentially, not applied to reasoning about such large-scale systems and their interfaces. We intend to explore this deficiency by researching
the technical, organizational, and social challenges of specifying and verifying interfaces in system ecosystems. In so doing, we will drive the use of verification techniques and improve the reliability of large systems.
Complex systems ecosystems and their interfaces are some of the most intricate and critical information ecosystems in existence today, and are highly dynamic and constantly evolving. We aim to understand how the interfaces between the components constituting these ecosystems work, and to verify them against their intended use. This research will be
undertaken through a collection of different themes covering systems topics where interface is crucially important, including critical code, communications and security protocols, distributed systems and networks, security policies, business ecosystems, and even extending to the physical architecture of buildings and networks. These themes are representative of the problem of specifying and reasoning about the correctness of interfaces at different levels of abstraction and criticality.
Interfaces of each degree of abstraction and criticality can be studied independently, but we believe that it will be possible to develop a quite general, uniform account of specifying and reasoning about them. It is unlikely that any one level of abstraction will suggest all of the answers: we expect that the work of the themes will evolve and interact
in complex ways.
Planned Impact
1. Who will benefit from this research? 2. How will they benefit from this research?
The beneficiaries of this research fall into the following groups: academic and industrial researchers; engineers analyzing and verifying code bases; systems architects and developers; managers with responsibility for structuring (possibly large, complex) organizations in the public and private sectors; policy-makers and regulators.
In the short term, the main beneficiaries of this research will be academic and industrial researchers in program verification, security, distributed systems, and management science. This benefit will derive from new scientific tools and methodologies and new formulations of research challenges, in which closely related problems concerned with the interfaces between communicating systems can be understood with a common conceptual framework. This impact will be achieved through the
well-established academic and scientific dissemination routes, including publications in top-rank conferences and journals and research seminars, as well as workshops with stakeholders, and other speaking opportunities. This will further reinforce the UK's leading position in verification research.
London is the global centre for the deployment of program analysis and verification techniques within the operations of the major technology companies such as Facebook and Amazon. These companies operate complex distributed systems, recognize the need to reason about their interactions, and need to employ suitably qualified staff to deliver this. IRIS will stimulate further investment in verification technologies and their deployment in London and will develop a pipeline
of researchers able to take forward a new, interdisciplinary field of systems verification, so reinforcing the UK's leading position in this important technology.
In the medium term, systems architects and developers in technology companies can hope to have system analysis tools --- for analysing and/or verifying the structure of their ecosystems via analysing and/or verifying the properties of system interfaces and the information flows across them --- of effectiveness/efficiency, and rigorous basis, that is
comparable to that of Facebook's recently open-sourced INFER tool (https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/). We anticipate also that IRIS will lead to subsequent research projects that will further develop its
ideas in its original and other directions and that these projects will train more staff, so continuing the pipeline of staff to out client technology companies.
In the long term, managers with responsibility for structuring (possibly large, complex) organizations in the public and private sectors will benefit from both improved understanding within their communities of the significance of good information-flow design for the effective operation of complex organizations and from the availability of conceptual tools
to support their decision that reflect this understanding. All of this should lead to improved efficiency and reliability of the services they offer to society, so helping to improve quality of life and commercial/creative output.
Similarly, policy-makers and regulators (especially in respect of sectors such as security and critical infrastructure) will benefit from improved understanding of the potential sources of vulnerability (to threats to efficiency, reliability, and security) in the complex ecosystems of systems upon which the smooth function of society depends. They will also benefit from conceptual tools to support their design of policy and regulatory mechanisms intended to ensure, for example,
adequate investment by the ecosystem stakeholders to ensure that systems communicate with sufficient integrity. Thus the robustness of society's critical infrastructure will be reinforced.
The beneficiaries of this research fall into the following groups: academic and industrial researchers; engineers analyzing and verifying code bases; systems architects and developers; managers with responsibility for structuring (possibly large, complex) organizations in the public and private sectors; policy-makers and regulators.
In the short term, the main beneficiaries of this research will be academic and industrial researchers in program verification, security, distributed systems, and management science. This benefit will derive from new scientific tools and methodologies and new formulations of research challenges, in which closely related problems concerned with the interfaces between communicating systems can be understood with a common conceptual framework. This impact will be achieved through the
well-established academic and scientific dissemination routes, including publications in top-rank conferences and journals and research seminars, as well as workshops with stakeholders, and other speaking opportunities. This will further reinforce the UK's leading position in verification research.
London is the global centre for the deployment of program analysis and verification techniques within the operations of the major technology companies such as Facebook and Amazon. These companies operate complex distributed systems, recognize the need to reason about their interactions, and need to employ suitably qualified staff to deliver this. IRIS will stimulate further investment in verification technologies and their deployment in London and will develop a pipeline
of researchers able to take forward a new, interdisciplinary field of systems verification, so reinforcing the UK's leading position in this important technology.
In the medium term, systems architects and developers in technology companies can hope to have system analysis tools --- for analysing and/or verifying the structure of their ecosystems via analysing and/or verifying the properties of system interfaces and the information flows across them --- of effectiveness/efficiency, and rigorous basis, that is
comparable to that of Facebook's recently open-sourced INFER tool (https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/). We anticipate also that IRIS will lead to subsequent research projects that will further develop its
ideas in its original and other directions and that these projects will train more staff, so continuing the pipeline of staff to out client technology companies.
In the long term, managers with responsibility for structuring (possibly large, complex) organizations in the public and private sectors will benefit from both improved understanding within their communities of the significance of good information-flow design for the effective operation of complex organizations and from the availability of conceptual tools
to support their decision that reflect this understanding. All of this should lead to improved efficiency and reliability of the services they offer to society, so helping to improve quality of life and commercial/creative output.
Similarly, policy-makers and regulators (especially in respect of sectors such as security and critical infrastructure) will benefit from improved understanding of the potential sources of vulnerability (to threats to efficiency, reliability, and security) in the complex ecosystems of systems upon which the smooth function of society depends. They will also benefit from conceptual tools to support their design of policy and regulatory mechanisms intended to ensure, for example,
adequate investment by the ecosystem stakeholders to ensure that systems communicate with sufficient integrity. Thus the robustness of society's critical infrastructure will be reinforced.
Organisations
- University College London (Lead Research Organisation)
- UNIVERSITY OF BIRMINGHAM (Collaboration)
- Amazon Web Services (UK) (Project Partner)
- GridPP (Project Partner)
- Facebook (United States) (Project Partner)
- Methods Group (Project Partner)
- Hewlett-Packard (United Kingdom) (Project Partner)
- BT Group (United Kingdom) (Project Partner)
Publications
Brunet P.
(2019)
A kleene theorem for nominal automata
in Leibniz International Proceedings in Informatics, LIPIcs
Bujorianu M
(2021)
Stochastic Safety for Markov Chains
in IEEE Control Systems Letters
Bujorianu M
(2022)
Modelling and Control of Complex Cyber-Physical Ecosystems
in IFAC-PapersOnLine
Carbonneaux Q
(2022)
Applying formal verification to microkernel IPC at meta
Caulfield T
(2021)
Engineering Ecosystem Models: Semantics and Pragmatics
Caulfield T
(2022)
Meta-modelling for Ecosystems Security
Caulfield T
(2022)
Modelling Organizational Recovery
Description | We have developed a comprehensive, coherent, and applicable account of the concept of interface in ecosystems of systems. This builds on an underlying theory of systems/ecosystems. We have developed associated 'local reasoning' principles and tools that track the compositional structure of ecosystems as characterized by the interfaces between systems. Along with this, we have developed a range of foundational approaches/analyses in the area of the philosophy and methodology of (formal/mathematical) modelling. These methodologies support the modelling and analysis of complex compositions of systemes. |
Exploitation Route | Support for formulating and implementing policy frameworks for regulating complex ecosystems of systems. |
Sectors | Digital/Communication/Information Technologies (including Software) Other |
URL | http://www.cs.ucl.ac.uk/staff/D.Pym/current.html |
Description | Applications to verification and reasoning tools in Facebook (meta). Applications to verification and reasoning tools in Amazon AWS. |
First Year Of Impact | 2019 |
Sector | Digital/Communication/Information Technologies (including Software),Security and Diplomacy |
Description | House of Commons Evidence - Challenges in implementing digital change |
Geographic Reach | National |
Policy Influence Type | Contribution to a national consultation/review |
URL | https://committees.parliament.uk/publications/8146/documents/83439/default/ |
Description | North East Local Economic Partnership Expert Contributor. |
Geographic Reach | Local/Municipal/Regional |
Policy Influence Type | Contribution to a national consultation/review |
URL | https://www.northeastlep.co.uk/the-plan/ |
Title | Artifact for "Challenges in Empirically Testing Memory Persistency Models" |
Description | Presented here are the litmus tests, auxiliary scripts, and output data constituting the artifact accompanying the paper titled 'Challenges in Empirically Testing Memory Persistency Models,' published in ICSE NIER'24. For detailed information, please refer to the README. |
Type Of Material | Database/Collection of data |
Year Produced | 2023 |
Provided To Others? | Yes |
URL | https://zenodo.org/doi/10.5281/zenodo.10427124 |
Description | Birmingham |
Organisation | University of Birmingham |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Collaborative research and dissemination. |
Collaborator Contribution | Collaborative research and dissemination. |
Impact | Categorical Proof-theoretic Semantics. In press, Studia Logica, 2024. |
Start Year | 2021 |
Title | Artifact for "Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs", PLDI 2023 |
Description | Artifact for PLDI 2023 paper, "Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs" |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
URL | https://zenodo.org/record/7711066 |
Title | C4 |
Description | C4 is a tool for automatically searching for bugs in C compilers. Specifically, it searches for bugs related to the compilation of _concurrent_ C programs. It works by (1) generating a corpus of small concurrent C programs and exhaustively simulating them to determine their correct outputs, (2) transforming each small program into a large program by applying a series of semantics-preserving mutations, and (3) running each large program through a variety of compilers and checking whether any incorrect outputs can be observed. C4 was presented at the ISSTA 2021 conference and will shortly appear in an STVR article. Its lead author is Matthew Windsor (RA on the IRIS project), and it is co-authored by Alastair Donaldson and John Wickerson (Investigators on the IRIS project). |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | C4 was able to uncover some real bugs in C compilers, which we have reported to the vendors. |
URL | https://github.com/c4-project |
Title | SysMods package for the Julia language |
Description | This is an ongoing development project associated with various projects over several years, 2015-current. |
Type Of Technology | Software |
Year Produced | 2024 |
Open Source License? | Yes |
Impact | A package for the Julia modelling language that implements the Distributed Systems Metaphor as described in many theoretical papers associated with this project. |
URL | https://github.com/tristanc/SysModels |
Title | The semantics of Shared Memory in Intel CPU/FPGA |
Description | The aim of this artefact is to demonstrate the claims made in the paper "The Semantics of Shared Memory in Intel CPU/FPGA Systems". This manual is divided into two parts: Getting Started Guide which should be finished in 30 minutes and a section where we will provide the Step by Step Instructions by which the paper instructions can be reproduced. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
URL | https://zenodo.org/record/5468872 |
Description | Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_files_for_View-Based_Owicki-Gries_Reasoning_for_Pers... |
Description | Anushri Gupti was invited to talk at the Alan Turning Institute workshop on Sustainable Cities |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
Results and Impact | Talk on Digital Twins at the workshop: This is a scoping workshop activity centred on the theme of 'Cities' that examines the role of data science and artificial intelligence in paving the way for sustainable cities. Aspects of sustainability in cities include mobility, energy, and climate with central pillars of equality, security, and data privacy. Two-thirds of humanity are expected to live in cities in 2050. These are cultural and business centres but are also major consumers of natural resources and producers of emissions. To make cities more resource-efficient and environment friendly, these different aspects of sustainability need to be considered jointly instead of the currently silo-ed approach. The workshop is structured under four themes: |
Year(s) Of Engagement Activity | 2023 |
URL | https://www.turing.ac.uk/events/ai-and-sustainable-cities |
Description | Associated editor for the track "Digital Innovation, Entrepreneurship, and New Business Models", International Conference on Information Systems |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | • Associated editor for the track "Digital Innovation, Entrepreneurship, and New Business Models", International Conference on Information Systems |
Year(s) Of Engagement Activity | 2021 |
Description | Brotherston ASL PC 2022 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | PC member. Workshop on Advancing Separation Logic (ASL), 2022. |
Year(s) Of Engagement Activity | 2022 |
Description | Cambridge University Executive Education |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Industry/Business |
Results and Impact | Cambridge University Executive Education: Dr. Will Venters talking about digital ecosystems / interfaces with executives. |
Year(s) Of Engagement Activity | 2018 |
Description | DIIESL - Digital Infrastructure, Innovation and Economy Seminars London (DIIESL) |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
Results and Impact | Various seminars with internationally renowned academics in Information Systems and junior researchers considering a particular topic. For the first seminar (On digital innovation) 173 people applied to attend and joined the mailing list (all received the Youtube version). Around 40-50 people attended the live-streamed event. |
Year(s) Of Engagement Activity | 2020 |
URL | https://www.diiesl.org/ |
Description | Discussion in Forbes business magazine on the challenges of integrating robotic process automation into business processes. |
Form Of Engagement Activity | A magazine, newsletter or online publication |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Interview for Forbes Magazine. Quoted and photograph in the magazine. |
Year(s) Of Engagement Activity | 2020 |
URL | https://www.forbes.com/sites/davidhowell1/2020/02/28/would-you-work-with-a-robot/#5fd9a8013482 |
Description | Fundación Ramón Areces |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Fundación Ramón Areces (Madrid): Dr. Will Venters consulting talking about the challenges of digital interfaces. |
Year(s) Of Engagement Activity | 2018 |
Description | Future Factory |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Industry/Business |
Results and Impact | Future Factory - 3 day masterclass by Dr. Will Venters on Digital Transformation talking to CDO and CIOs from major manufacturing plants about the challenges of digital interfaces. |
Year(s) Of Engagement Activity | 2018 |
Description | INI Concurrency Meeting 2022 |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | This was a 2-day workshop held at the Isaac Newton Institute in Cambridge, to bring together researchers from academia and industry who work on the theory and practice of concurrency. Attendees were mostly from the south of England, but some came from the wider UK and a handful travelled in from Europe. I don't know any specific outcomes of the event, but I expect several people will have made new connections with those who share research interests, which may well spark further collaborations. |
Year(s) Of Engagement Activity | 2022 |
URL | https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fjohnwickerson.github.io%2Fcw2022.h... |
Description | IRIS @ QMUL Industry Day |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Regional |
Primary Audience | Industry/Business |
Results and Impact | Presentation by Prof Edmund Robinson of a poster about the IRIS project at the QMUL Industry Day. |
Year(s) Of Engagement Activity | 2018 |
Description | Invited Lecture by Byron Cook at OOPSLA/SPLASH 2018 |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Formal reasoning about the security of Amazon Web Services Place: OOPSLA/SPLASH 2018 keynote lecture Date: November 9, 2018 |
Year(s) Of Engagement Activity | 2018 |
Description | Invited talk to Finding Real Bugs in Big Programs with Incorrectness Logic. PL group, Department of Computer Science, University of Bristol, UK. June 2023. |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
Results and Impact | Quang Loc Le invited to a talk on Finding Real Bugs in Big Programs with Incorrectness Logic. PL group, Department of Computer Science, University of Bristol, UK. June 2023. |
Year(s) Of Engagement Activity | 2023 |
Description | Invited talk to Incorrectness Logic and Underapproximation: Foundations of Bug Catching. Formosan Summer School on Logic, Language, and Computation. National Taiwan University. Aug 2023. |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Quang Loc Le gave a talk at the Incorrectness Logic and Underapproximation: Foundations of Bug Catching. Formosan Summer School on Logic, Language, and Computation. National Taiwan University. Aug 2023. |
Year(s) Of Engagement Activity | 2023 |
Description | Invited talk to Incorrectness Logic and Underapproximation: Foundations of Bug Catching. TutorialFest POPL 2023 - Boston, Massachusetts, United States. Jan 2023. |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | Quang Loc Le invited to talk in Incorrectness Logic and Underapproximation: Foundations of Bug Catching. TutorialFest POPL 2023 - Boston, Massachusetts, United States. Jan 2023. |
Year(s) Of Engagement Activity | 2023 |
Description | Keynote Lecture by David Pym at SYSMICS 2018, Vienna |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Substructural logics: semantics, proof theory, and applications 26-28 February 2018, Vienna (Austria) Second SYSMICS Workshop Invited Lecture: David Pym Title: Logic as a modelling technology: resource semantics, systems modelling, and security Abstract: The development of BI, the logic of bunched implications, together with its resource semantics, led to the formulation of Separation Logic, which forms the basis of the Infer program analyser deployed in Facebook's code production. However, this rather successful story sits within a broader, quite systematic logical context. I will review the (family of) logics, including process logics, that are supported by resource semantics, explaining their more-or-less uniform meta-theoretic basis and illustrating their uses in a range of modelling applications, including access control, systems security, and workflow simulation. |
Year(s) Of Engagement Activity | 2018 |
URL | https://sysmics.logic.at/invited |
Description | Lecture Course at SYSMICS Summer School, Les Diablerets, 2018 |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Four lectures on logic as a modelling technology. Impact on PhD students. https://www.dropbox.com/sh/jl3wr3vgx68ajvb/AAA_tT9b7tglSm0fTRHJEqNia?dl=0 |
Year(s) Of Engagement Activity | 2018 |
URL | https://mathsites.unibe.ch/sysmics/ |
Description | Participation in an activity, workshop or similar - Future Factory |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Executive Education on the impact of digital interfaces to CxO level staff involved in digital transformationhttps://www.thefuturefactory.com/will-venters |
Year(s) Of Engagement Activity | 2022 |
URL | https://www.thefuturefactory.com/will-venters |
Description | Plenary Lecture by Byron Cook at FLoC 2018 |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Lecture by Byron Cook. Formal reasoning about the security of Amazon Web Services Place: FLoC Plenary Date: July 16, 2018 |
Year(s) Of Engagement Activity | 2018 |
Description | Presentation at Tommy Flowers Network TFNetworkSpring22 Digital Transformation conference (Run by BT and DigitLab) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
Results and Impact | In this wide ranging talk I will introduce the challenges and opportunities of researching digital transformation: How can researchers go beyond traditional research topics? How can we research digital ecosystems? How can we develop new theories of digital transformation? What should we researchers be thinking about? How can we engage with industry better to find new insight? How do we ask the right questions? How do we remain critical of assumptions made by industry? |
Year(s) Of Engagement Activity | 2022 |
URL | https://tommyflowersnetwork.blogspot.com/2022/01/virtual-conference-digital.html |
Description | Presentation at a Conference: Reasoning over permissions regions in concurrent separation logic" (joint work with J. Brotherston, J. Wickerson, A. Hobor), Days in Logic 2020, Lisbon |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | Presentation at a conference, share knowledge, sparkle a discussion and develop new ideas The paper was accepted as a short presentation, something that was not in the plans of the conference. It meant that the reviewers liked this work, which Diana Costa had described as very preliminary. |
Year(s) Of Engagement Activity | 2020 |
Description | Presentation in the professional conference MapCamp of our research on Wardley Maps |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | Presentation in the professional conference MapCamp of our research on Wardley Maps |
Year(s) Of Engagement Activity | 2020 |
Description | Presentation in the professional conference MapCamp of our research on Wardley Maps (Sadlers Wells, London, October 2019) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | • Presentation in the professional conference MapCamp of our research on Wardley Maps (Sadlers Wells, London, October 2019) |
Year(s) Of Engagement Activity | 2019 |
URL | https://www.map-camp.com/_pages/2019-10-15_London/ |
Description | Pym CODASPY PC 2022 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | The 12th ACM Conference on Data and Application Security and Privacy April 25 - 27, 2022. Baltimore-Washington DC Area, United States. |
Year(s) Of Engagement Activity | 2022 |
URL | http://www.codaspy.org/2022/index.html |
Description | Pym GameSec PC 2022 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Programme Committee 2021 Conference on Decision and Game Theory for Security |
Year(s) Of Engagement Activity | 2021 |
URL | https://www.gamesec-conf.org |
Description | Pym WEIS PC 2021 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Programme Committee, WEIS 2021 |
Year(s) Of Engagement Activity | 2021 |
URL | https://weis2021.econinfosec.org |
Description | Researchers from the IRIS group organised the the London Hopper Colloquium |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | Regional |
Primary Audience | Professional Practitioners |
Results and Impact | An event about women in Computer Science, including equity, diversity and inclusion. |
Year(s) Of Engagement Activity | 2023 |
URL | https://www.bcs.org/events-calendar/2023/may/london-hopper-colloquium-2023/ |
Description | Symposium on proof-theoretic semantics participation |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | I gave a talk about shared work with David Pym to get feedback on it and listened to talks on current research. |
Year(s) Of Engagement Activity | 2022 |
URL | https://sites.google.com/view/pts-symposium-uk/ |
Description | Talk at " Compositional Incorrectness Proving at Scale.School of Computing" - National University of Singapore. Aug 2023. |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Undergraduate students |
Results and Impact | Quang Loc Le invited to talk at Compositional Incorrectness Proving at Scale.School of Computing - National University of Singapore. Aug 2023. |
Year(s) Of Engagement Activity | 2023 |
Description | The Leadership challenges of homeworking | LSE Management Blog |
Form Of Engagement Activity | Engagement focused website, blog or social media channel |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | These are general management blogs targeting practitioners and academics in the management and information systems space. While I do not have full statistics I know that I had around 4000 views the "leadership challenge of homeworking" post on Linkedin. "What automation can do for small business" was viewed on linked in around 1300 times. The blogs were widely cited - Indeed I know through personal connections that the Institute of Cancer Research used the Homeworking blog in making decisions on staff working during COVID. |
Year(s) Of Engagement Activity | 2020 |
URL | https://blogs.lse.ac.uk/management/2020/06/23/how-leaders-can-support-their-staff-after-long-term-ho... |
Description | What automation can do for small businesses - Binary Blurring Blog |
Form Of Engagement Activity | Engagement focused website, blog or social media channel |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | These are general management blogs targeting practitioners and academics in the management and information systems space. While I do not have full statistics I know that I had around 4000 views the "leadership challenge of homeworking" post on Linkedin. "What automation can do for small business" was viewed on linked in around 1300 times. The blogs were widely cited - Indeed I know through personal connections that the Institute of Cancer Research used the Homeworking blog in making decisions on staff working during COVID. |
Year(s) Of Engagement Activity | 2020 |
URL | https://binaryblurring.com/2020/06/24/what-automation-can-do-for-small-businesses/ |
Description | • Associated editor for the track "The Internet of Everything (IoE): The Economic, Social, and Environmental Impact of Pervasive Connectivity", European Conference on Information Systems (Stockholm, 2019) |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Policymakers/politicians |
Results and Impact | Associated editor for the track "The Internet of Everything (IoE): The Economic, Social, and Environmental Impact of Pervasive Connectivity", European Conference on Information Systems (Stockholm, 2019) |
Year(s) Of Engagement Activity | 2019 |
Description | • Reviewer of papers in European Conference on Information Systems, International Conference on Information Systems, European Journal of Information Systems |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
Results and Impact | Reviewer of papers in European Conference on Information Systems, International Conference on Information Systems, European Journal of Information Systems |
Year(s) Of Engagement Activity | 2020 |