PhD defense, Computer science and engineering, Alejandro Gómez Londoño

Communicating systems have become ubiquitous in today's society. Unfortunately, the complexity of their interactions makes them particularly prone to failures such as deadlocked states
caused by misbehaving components, or memory exhaustion due to a surge in message traffic (malicious or not).

These vulnerabilities constitute a real risk to users, with
consequences ranging from minor inconveniences to the possibility of
loss of life and capital.

This thesis presents results that aim to increase the reliability of communicating systems.
First, we implement a choreography language that can, by construction, only describe deadlock-free systems.

Second, we develop a cost semantics to prove programs free of out-of-memory errors.

Lastly, we improve both results by using novel semantic approaches that strengthen key theorems and facilitate further proof development.

All of these results are formalized in the HOL4 theorem prover and integrated with the CakeML verified stack.