# Accelerated Verification of Concurrent Systems

## Maurice Laveaux

Promotores: dr.ir. Tim Willemse (TU/e)

and prof.dr.ir. Jan Friso Groote (TU/e)

Eindhoven University of Technology

Date: *22 November, 2022*

Thesis: PDF

#### Summary

concurrent systems where interaction between computers must also be taken into account.A key ingredient to ensure the correctness of software is to specify its

behaviour in a way that can be analysed formally. In our setting we specify this

behaviour as processes using a process algebra. Model checking is a technique

that considers a model of the specification and automatically verifies that the

specified behaviour matches the intended behaviour, which must also be

specified. The behavioural model of a specification is in our case defined by a

state space consisting of all possible states of the system and a transition

relation between states that defines the (nondeterministic) choices in each

state. A major obstacle for the verification of practical systems is the size of

these state spaces. In this dissertation we investigate several ways to tackle this

problem.We identify several issues pertaining to the soundness and performance in

existing antichain-based refinement algorithms and propose new, correct,

antichain-based algorithms. Refinement is a model checking technique that checks

whether the behaviour of one process refines the behaviour of another process.

It is the basis of a stepwise development methodology in which the correctness

of a system can be established by proving, or computing, that a system refines

its specification.We define a decomposition technique to effectively obtain the state space of a

so called monolithic process. A monolithic process is a single recursive

equation with data parameters, which only uses non-determinism, action

prefixing, and recursion. For the decomposition we can show that a composition

of these processes is strongly bisimilar to the monolithic process under a

suitable synchronisation context. Minimising the resulting processes before

determining their composition can be used to derive a state space that is

smaller than the one obtained by a monolithic exploration.

Another model checking technique considers a specification and a property

written in a formal language and decides whether the specification satisfies

this property, which is called the model checking problem. Parity games are a

typical encoding used for this model checking problem. We formalise how to use

on-the-fly solving techniques of parity games can be applied during the

exploration process, and show that this can help to decide the decision problem

more efficiently by terminating early.

Finally, we propose a thread-safe term library that can be used as the basis for

concurrent model checking algorithms, including the previously described ones.

Terms are one of the fundamental data structures used for computing and

therefore are also extensively used in the toolset where our techniques have

been implemented. To this end we define a new efficient multiple-reader/single

write mutual exclusion algorithm that has been shown to be correct used model

checking. Using the new library in an existing state space generation tool, very

substantial speed ups can be obtained.