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 (EP/K008528/1, 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.