In model-driven development, the automated generation of a multi-threaded program based on a model specifying the intended system behaviour is an important step. Verifying that such a generation step semantically preserves the specified functionality is hard. In related work, code generators have been formally verified using theorem provers, but this is very time-consuming work, should …continue reading

In this talk, I will present SIGmA (SAT sImplification on GPU Architectures), a preprocessor to accelerate SAT solving that runs on NVIDIA GPU(s). We discuss the tool, focusing on its full functionality, including new simplifications and multi-GPU support with load balancing mechanism. SIGmA performs various types of simplification, such as variable elimination, subsumption elimination, blocked …continue reading

Branching bisimulation is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. While it is slightly coarser than weak bisimulation, it has the advantage that there is a unique branching bisimulation equivalence quotient that can be found efficiently. With m the number of transitions and n the number of states, …continue reading

The spectrum of branching-time relations for probabilistic systems has been investigated thoroughly by Baier, Hermanns, Katoen and Wolf (2003, 2005), including weak simulation for systems involving substochastic distributions. Weak simulation was proven to be sound w. r. t. the liveness fragment of the logic PCTL\X , and its completeness was conjectured. We revisit this result …continue reading

This paper presents an application of the formal modelling and model checking toolkit mCRL2 and the model-based testing tool JTorX in the signalling domain. The mCRL2 toolkit is used to formally model the behaviour of a system at the core of signalling solutions: the interlocking. The model of the interlocking is validated through model-based testing. We …continue reading

The O(m log n) algorithm for branching bisimulation devised by Groote/Jansen/Keiren/Wijs was primarily directed towards Kripke structures and not to labelled transition systems. To verify branching bisimulation for LTSs an explicit translation is made to Kripke structures. This means that the complexity for LTSs actually is O(m (log n + log |Act|)) and in practice the memory requirements are …continue reading

We discuss how to solve reachability problems either in BDD based symbolic model checking (by NuXMV) or by bounded model checking using SMT solving. We provide several examples, mainly from the practical assignments of the course Automated Reasoning, over the years. These include deadlock checking in hardware and infinite branching.

Probabilistic labelled transition systems combine the expressiveness of Markov chains and processes. We are interested in finding a suitable trace equivalence for such systems, which becomes non-trival once non-determinism is introduced. For this search I have axiomatised one of the equivalences, based on weighed traces, which is a complete axiomatisation, to gain a better understanding …continue reading

In 1992, Bradfield and Stirling presented a tableaux-based approach to local model checking of infinite-state systems that is sound and complete. When trying to apply this approach to model-checking timed and hybrid automata against mu-calculus properties we observed that the approach is not practical. In this talk I will explain Bradfield and Stirling’s proof system, …continue reading