Logic and Semantics

Introduction
The Logic and Semantics group specialises in the logical, mathematical and statistical foundations of computer science, with a breadth and depth of expertise almost unmatched in the UK. They tackle the hard problems inherent in discovering the power and limitations of computer systems, and how principled design based on the right mathematical models might make them more robust and secure. The group has an international reputation in the mathematical modelling of computational systems, focusing on the models themselves, and their use to prove properties of particular systems or properties of systems in general. They collaborate with NASA and with Intel on novel mathematical techniques for modelling and reasoning about dynamical systems.

The group's expertise covers a broad range from complexity, through automated reasoning, concurrent and distributed systems, formal methods in Human-Computer Interaction to verification of systems software and logic. A major area of research concerns separation logic, a formalism of program dynamics extending Hoare's logic which addresses difficulties in reasoning about pointer data structures, and its use for program verification.

Members of the group are engaged in a number of international projects funded by EPSRC and international industry. The group's work on separation logic is currently supported by three EPSRC grants. The interdisciplinary Computational Logic for Control project, a collaboration between Queen Mary's Computer Science and Maths departments, Qinetiq, NASA Langley, Intel Research Cambridge and the Automated Reasoning Group in the Computer Laboratory at the University of Cambridge, aims to develop a computational logic framework for control in engineering applications, for example in avionics or novel computational architectures. The Pragmatics project is developing a logic for the field of linguistics known as pragmatics: that is, the assignment of meaning to verbal communications. They also have significant research directions on concurrency theory, security and program analysis funded by EPSRC. Group members also serve as scientific advisors for web-service working groups of W3C, the main standardisation body of the World-Wide Web, on future standards of web-based programming.

The group is the hub of the London Separation Logic Community, for which it hosts weekly meetings. In addition, once every two months or so they hold a Resource in East London (REaL) meeting with colleagues from Bath, Birmingham, Cambridge, Imperial and Sussex.

Members of the research group contribute to specialised research-led modules to several of the advanced Masters programmes run by the Department.

Visit the Logic and Semantics group webpages