Alejandro Gómez Londoño, Data- och informationsteknik

Choreographies and Cost Semantics for Reliable Communicating Systems

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 two results that aim to increase the reliability of communicating systems. First, we implement a choreography language which by construction can only describe systems that are deadlock-free. Second, we develop a cost semantics to prove programs free of out-of-memory errors. Both of these results are formalized in the HOL4 theorem prover and integrated with the CakeML verified stack.
Alejandro Gómez Londoño tillhör avdelningen för Formella metoder vid Data- och informationsteknik.

Diskussions ledare

Assistant professor Tjark Weber, Uppsala University, Sweden.

Länk till seminariet online

Länk till publikation

Kategori Licentiatseminarium
Plats: Online, link above
Tid: 2020-08-27 10:00
Sluttid: 2020-08-27 12:00

Sidansvarig Publicerad: on 19 aug 2020.