REMS: Rigorous Engineering for Mainstream Systems
How can we use rigorous mathematics to improve the quality of mainstream
computer systems? REMS (Rigorous Engineering for Mainstream Systems),
is a 6-year EPSRC-funded Programme Grant
2013-2019) to do just that, bringing
together an exciting combination of researchers in systems
(architecture, operating systems, and networks) and in semantics
(programming languages, automated reasoning, and verification) at
Cambridge, Imperial, and Edinburgh.
We're finally in a position to scale up and apply mathematically rigorous semantics to mainstream systems:
The project is focussed on
lightweight rigorous methods: precise specification (post hoc and during design) and testing against specifications, with full verification only where that is feasible. The project emphasises building useful (and reusable) semantics and tools.
We aim to understand how to build accurate full-scale mathematical
models of some of the key computational abstractions (processor
architectures, programming languages, and concurrent OS interfaces),
and how these can be used for new verification research, to build
tools that are applicable to real systems, and to enable new systems
and programming language research. Supporting all this, we are also
working on new specification tools and their foundations.
- to develop rigorous semantics for real systems
(especially key interfaces: processor architectures, programming language definitions, and concurrent OS libraries); and
- to develop real systems and do systems research using rigorous semantics and tools based on it.