Events at MetaForum MF 12

A model of multicopy semantics of low level memory operations is made in mCRL2. These memory operations can be relaxed, release, acquire and sequentially consistent, which determine whether these operations can be executed before or after surrounding instructions. Using this model it is investigated which semantics the read and write operations of Peterson’s mutual exclusion algorithm must have to work …continue reading

xMAS is a language initially proposed by Intel for architectural modelling and verification. The main feature of xMAS is to enable a boolean encoding of liveness that can be efficiently checked using SAT-based techniques. xMAS is restricted to a small set of well-defined primitives. Recently, Verbeek et al. extended this approach to state machines. In …continue reading