Research

How the site is organised

The site is intentionally structured as hubs and detail pages. Hubs provide a thematic map; detail pages provide focused content: a glossary, a few sections of explanation, and a list of common pitfalls. If you arrive via a specific workshop page or note, this hub is the fastest way to rebuild context.

• NotesCompact explanations designed to be revisited.
• ProjectsProject-style topics with internal reading paths.
• PublicationsGrouped publication summaries and one detailed page.

Formal Methods

“Formal methods” is a broad label. In this site’s context, it means using explicit models of behaviour to support clear reasoning. The model can be as simple as a small transition system or as rich as an operational semantics with a proof theory. The practical aim is to surface assumptions early: ordering constraints, failure behaviour, concurrency, and resource limitations.

A useful litmus test is compositionality: can the effects of composition be understood from the parts? If a property is not compositional, it may still be interesting, but it will be hard to use in a workflow that scales. The pages here therefore emphasise properties and modelling choices that make composition tractable.

• Model checking primerState exploration as an engineering check.
• Graph rewriting and SOSRules-as-semantics for behavioural models.

Behavioural Types

Behavioural types treat interaction itself as something that can be specified. Instead of saying “a function takes an int and returns a string”, a protocol description can state “a component performs this sequence of message exchanges, with branching choices and concurrency constraints”. When communication becomes explicit, many common integration bugs become easier to reason about.

A key advantage is that protocols offer structure: a contract that can be checked at boundaries and used to guide implementation. On this site, protocols appear as session types, behavioural contracts, and interface specifications for components.

• Session types and protocolsProtocols-as-types for concurrency and messaging.
• Behavioural contractsAssume/guarantee framing and compatibility.

Component Models

Component models are about structure: what a component is, how components connect, and what “glue” means. Many systems are built by composing independently developed parts, so the interface between parts becomes a first-class design object. A component model makes that interface explicit, allowing composition to be defined and meaningful questions to be asked about global behaviour.

The site uses BRiCoS as a representative project/topic page: a building-block perspective that emphasises compositional operators. Another angle is the BIP framework, which separates behaviour, interaction, and priority to make coordination explicit.

• BRiCoS topic pageBuilding blocks for rigorous design of concurrent software.
• Component systems and BIPA model for glue and coordination.

Verification Workflows

Verification is not a single technique; it is a workflow. The question is rarely “can it be proven?” and more often “what is the cheapest check that prevents costly misunderstandings?”. Sometimes the right tool is a small invariant and a few runtime checks; sometimes it is a model-checking run on an abstract model; sometimes it is a proof about a critical protocol.

This site emphasises workflows that are repeatable: choose a model, state properties, pick an analysis, interpret results, and iterate. The goal is not to do verification for its own sake, but to make design decisions explicit and make failures explainable.

• Session types & protocolsA project-style entry point into protocol reasoning.
• Publication summariesContext on why workflows are designed the way they are.

Method and approach

Most of the work described here follows a small loop:

• Make interaction explicitWrite down a protocol or contract at boundaries, even if it is initially informal.
• Choose a minimal modelPick the smallest semantics that still answers the question you care about.
• State properties earlySafety, liveness, and compatibility are easier to discuss before implementation details dominate.
• Pick a feasible checkUse abstraction to keep checks tractable; favour checks that are repeatable and explainable.
• Iterate with constraints in mindTreat performance, failure, and partial information as part of the model.

You can see this loop reflected throughout the notes: each note tries to separate definitions, intuition, and pitfalls. For a fast entry point, start with the model checking primer or the behavioural contracts note.