ChorEr: un analizzatore statico per generare Automi Coreografici da codice sorgente Erlang

Il recente sviluppo di applicazioni concorrenti e distribuite ha dato origine a un nuovo interesse verso il linguaggio Erlang (ed Elixir che si basa su una Erlang Virtual Machine BEAM) e verso altri linguaggi e paradigmi di programmazione che implementano nella loro logica l'uso di thread e di message passing. Il modello ad attori e le coreografie rivestono un ruolo importante nel futuro dei sistemi mobili e distribuiti: il modello ad attori è un modello concorrente sicuro e intuitivo; invece, le coreografie permettono di evitare sintatticamente alcuni degli errori tipici dei sistemi concorrenti (liveness, lock freedom e deadlocks freedom). In questa tesi viene presentato ChorEr, un tool di analisi statica per programmi in Erlang che genera degli Automi Coreografici, cioè degli automi a stati finiti che permettono una verifica semplificata delle proprietà citate.