Transformation techniques for constraint logic programs with applications to protocol verification

The contribution of this thesis consists in the extension of the techniques for the transformation of constraint logic programs and the development of methods for the application of these techniques to the proof of temporal properties of parameterized protocols. In particular, we first introduce a method for proving automatically the total correctness of an unfold/fold transformation by solving linear equations and inequations over the natural numbers. We also propose a transformation-based method for proving first order properties of constraint logic programs which manipulate finite lists of real or rational numbers. Then, we extend the standard folding transformation rule by introducing two variants of this rule. The first variant combines the folding rule with the clause splitting rule for obtaining a more powerful folding rule. The second variant is tailored to the elimination of the existential variables occurring in a clause. For the standard folding rule and its two variants we develop the corresponding algorithms for automating their application. Finally, we propose a program transformation framework for proving temporal properties of parameterized protocols. Using this framework we encode the protocols and the temporal properties we want to prove as logic programs, and then we use the unfold/fold transformation technique for proving whether or not the properties holds.

Il contributo di questa tesi consiste nell'estensione delle tecniche per la trasformazione dei programmi logici con vincoli e lo sviluppo di metodi per l'applicazione di queste tecniche alla prova di proprietà temporali di protocolli parametrizzati. Per prima cosa viene proposto un metodo per la prova automatica della correttezza totale delle trasformazioni che usano regole di unfolding e folding basato sulla risoluzione di sistemi di equazioni e disequazioni sui numeri naturali. In secondo luogo viene proposto un metodo trasformazionale per la prova di proprietà del primo ordine di programmi logici con vincoli che manipolano liste finite di numeri razionali o reali. Inoltre, viene estesa la regola di trasformazione detta folding introducendo due varianti: la prima, che combina la regola di folding standard con la regola detta di clause splitting, e la seconda, che ha lo scopo di eliminare le variabili esistenziali che occorrono in una data clausola. Per la regola di folding standard e per le estensioni che vengono proposte, vengono forniti i corrispondenti algoritmi che ne permettono l'applicazione automatizzata. Infine, viene proposto un framework per la prova di proprietà temporali dei protocolli parametrizzati. Utilizzando questo framework viene codificato il protocollo e la proprietà che si intende provare come un programma logico. In seguito, usando la tecnica di trasformazione attraverso le regole di unfold e fold, viene verificato se la proprietà vale o meno per il dato protocollo. La tesi è corredata di esempi per la dimostrazione delle tecniche proposte.