Software Architectures & Design Calculi

Research team @ HASLab, Univ. Minho

Model checking R/G programs in Alloy



When you run a program on your lap-top you "rely" on the operating system not letting any other program to interfere with your state space. But programs could be designed in a collaborative-style, with sub-programs helping each other over a shared state. (Example: on-the-fly garbage collection.)

Thus "no-interference" programming is just a special case of "allow-interference" programming. In the early 1980s, Cliff Jones proposed a dynamic extension to (static) Hoare logic: further to pre / post conditions, one could also specify interference of the environment via rely / guarantee conditions. Interest on R/G programming is growing a lot due to its potential for concurrency. But it has become clear that "allow-interference" programming has its subtleties, e.g. concerning non-termination.


In this project we would like to use Alloy to model the semantics of a simple imperative language with R/G commands and model-check their interference. The idea is to find design errors of (possibly non-terminating) R/G programs by analysing finite traces only.

Relevant literature