Concurrent systems are ubiquitous in our modern world, from usual online interactions between our devices and servers to distributed systems and automated production chains. Safety of communication protocols in concurrent systems is therefore a key point to ensure the reliability of systems we rely on a daily basis. Several models exist to represent concurrent systems; and several works build around those models to provide verification toolchains for their protocols. In this thesis, we provide extensions of safety properties for two such frameworks.

One is a framework based on behavioural types theory for the popular programming language Go. Since a broad range of errors arise from mixed use of shared memory and channel-based communication, we develop an extension to both the type system and the static verification tool to account for explicit memory locking mechanisms and direct-access shared memory primitives, in addition to channel-based communication primitives that were accounted for in previous works. The other is a newly reworked multiparty session types (MPST) framework for general concurrency use, for which we propose an extension to account for non-deterministic communications and to make use of the witness extraction capabilities of model checking tools. The tools we provide with our theories are, to our knowledge, respectively the first static verification framework for the Go language to uniformly analyse concurrency errors caused by a mix of asynchronous message-passing communications and shared memory accesses; and the first MPST toolchain to make use of witness extraction capabilities of model checking tools to link detected errors directly to the analysed program.