Events at MetaForum MF 12

–

Modern software systems are highly configurable, often having huge configuration spaces with myriads of valid configurations. Exhaustive testing is therefore not feasible in practice. A common approach towards a representative set of test configurations is by sampling the configuration space uniformly at random. In this talk I will showcase algorithms to sample configuration spaces given …continue reading

–

Abstract: Low Code Development Platforms, such as the Cordis SUITE, facilitate formal verification in software development for industrial automation. An automated translation from Cordis models to mCRL2 enables the for- mal verification of real-world industry models. However, this approach is not without challenges. The monolithic nature of the translation can lead to state space explosions …continue reading

–

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