Analisi della Liquidità nei contratti legali in Stipula

I contratti legali definiscono clausole che regolano le interazioni tra più parti e disciplinano la gestione di risorse patrimoniali. In questo contesto, la proprietà di liquidità garantisce che le risorse gestite da un contratto non rimangano permanentemente bloccate e che il loro valore possa tornare nella disponibilità di una delle parti coinvolte. In questa tesi studiamo tale proprietà nei contratti legali scritti in Stipula. Ne introduciamo la sintassi e la semantica operazionale, quindi formalizziamo le proprietà di k-Separate Liquidity e Liquidity, insieme a un sistema di tipi capace di descrivere simbolicamente il comportamento del contratto in esecuzione rispetto alle risorse gestite. Su questa base presentiamo due algoritmi per la verifica automatica della liquidità e realizziamo, in Python, un analizzatore che li implementa. Lo strumento consente di stabilire se un contratto soddisfa tali proprietà e di individuare eventuali situazioni di blocco permanente del valore.