Dennis Rizvić: Making MCA easily understandable with mCRL2
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
Julien Schmaltz: On the definition of block and idle for xMAS automata.
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