The group’s work focuses on developing, using and reasoning with visual notations with tool support (see the automated reasoning page under Current work). There are two main strands to our work: developing and using diagrammatic notations to express logical assertions and developing and investigating formal diagrammatic reasoning systems based on these notations.

The main thrust of our work on the modelling side is the development of diagrammatic notations for use with the Unified Modelling Language (UML) notations in software development.  One such notation is constraint diagrams, which was designed to express visually mathematical constraints such as system invariants and operation preconditions and postconditions.

Out of the investigation into constraint diagrams arose the visual notation spider diagrams. These are based on Venn and Euler diagrams and build on a long tradition of such notations.

The use of the diagrammatic notations in  modelling and reasoning will be made more practical with the development of sophisticated software tools. Currently a constraint diagram editor is available to download.  We have been awarded a substantial grant, in collaboration with the University of Kent, by the UK EPSRC, for a project entitled Reasoning with Diagrams. The aim of this project is to develop a framework, i.e. a collection of software tools, to support reasoning with a combination of diagrammatic and textual constraint notations, suitable for use by practitioners. The project began in July 2002 and runs for three years.

The group has developed collaborations with people and teams from all over the world. We are currently working in the following areas:
Formalisation
Modelling
Diagrammatic reasoning
Abstract and concrete diagrams
Usability
Generating diagrams
Implementation in PVS
Textual Languages
Projections
Linear logic
Combinatorics

The tutorial Advanced Visual Modelling has been delivered at many international conferences, most recently at ICSE'02.