Research interests
Research themes emphasised on this site include making system behaviour explicit (through models, semantics, and protocols), reasoning compositionally about interaction, and connecting formal checks to practical workflows.
- Behavioural modelsOperational descriptions of behaviour that make assumptions explicit.
- Interaction and protocolsOrdering, branching, and concurrency constraints at system boundaries.
- Contracts and compositionAssume/guarantee reasoning and compatibility of components.
- Verification workflowsAbstraction and repeatable checks that remain feasible.
Topics and methods
Internal links to pages that expand each theme.
- Formal methods How precise models support compositional reasoning and communication about behaviour.
- Behavioural types Protocols as types; how structure guides safe interaction in concurrent settings.
- Component models Interfaces, glue, and the difference between local correctness and system-level properties.
- Verification workflows From specification to model to checks that fit engineering constraints.
Selected themes
Several pages on this site repeatedly return to the same design questions: what does a component assume about its environment, what can be guaranteed under composition, and which checks provide the best signal under limited time and modelling budget. These themes appear across the Research and Projects hubs and are supported by short Notes intended as refreshers.
- Model checking primerA practical view of properties and abstraction.
- Behavioural contractsAssumptions and guarantees as interfaces.
- Component systems and BIPGlue and coordination as explicit artefacts.
For enquiries about this site
Enquiries about this site (corrections, navigation issues, and general feedback) should be sent to the site contact. This page does not publish personal contact details for individuals.
- About this siteStewardship and affiliation statement.
- ContactSite enquiries only.