Personal tools
You are here: Home Events Lab Lunch by Ian Stark

Lab Lunch by Ian Stark

— filed under:

REMS: Rigorous Engineering for Mainstream Systems

  • Lab Lunch
When Mar 31, 2015
from 01:30 PM to 02:30 PM
Add event to calendar vCal

I'll talk about the REMS project with which Brian Campbell and I are involved.

REMS is a collaboration between Cambridge, Imperial and Edinburgh that aims to "use rigorous maths to improve the quality of mainstream computer systems". It's funded by a six-year EPSRC programme grant and includes a range of participants familiar to LFCS --- notably site leaders Peter Sewell (Cambridge) and Philippa Gardner (Imperial).

The "rigorous maths" part of REMS covers many LFCS favourites, like semantics, verification and automated theorem provers.  By "mainstream", we mean concrete processor architectures (MIPS, ARM, Power), languages (C/C++) and systems programming issues (networking, concurrency, memory architectures).  There is an emphasis on lightweight methods rather than full verification everywhere: such as test suites automatically generated from precise specifications rather than formal proofs of functional correctness.

I'll give an overview of REMS and some of the project results, as well as the work in Edinburgh being done by Brian Campbell and myself on test generation for a customised MIPS processor using formal modelling in HOL and the Yices SMT solver.

Document Actions