Formalizzazione logica del paradigma di programmazione aggregata in Coq

Considerando un contesto ambientale in cui il numero di dispositivi a nostra disposizione è sempre maggiore, la programmazione aggregata si propone di programmare una rete di dispositivi definendo il suo comportamento globale, astraendo dal comportamento locale di ogni singolo dispositivo della rete. In questa metodologia, linguaggi e algoritmi praticamente utilizzabili vengono affiancati da garanzie di resilienza dimostrate formalmente. Tuttavia, tutte queste dimostrazioni sono finora state svolte in maniera manuale, e non meccanicamente controllata tramite proof assistant. Una formalizzazione del paradigma aggregato in un tale sistema come COQ, consentirebbe di controllare automaticamente le dimostrazioni già effettuate, e di effettuarne di nuove in maniera automatizzata e controllata. Lo scopo della tesi sarà di acquisire tutte le competenze relative alla formalizzazione logica della programmazione aggregata e implementare le conoscenze acquisite all'interno del proof assistant COQ, consentendo dimostrazioni del paradigma il più possibilmente automatiche.