The thesis studies the formal verification of temporal properties of safety and liveness of parametrized concurrent systems, with a special focus on programs that manipulate complex concurrent data structures in the heap. This work presents a formal framework based on deductive methods which cleanly separates the analysis of the program control flow from the data manipulated by the program. The program control flow is analyzed using novel specialized deductive verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, the techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. Additionally, the thesis explores the construction of decidable theories equipped with decision procedures that can automatically check the generated verification conditions for some complex concurrent data structures. Finally, the whole framework is evaluated over some safety and liveness properties for a collection of mutual exclusion protocols and concurrent pointer-based data structures.
Alejandro Sánchez was advised by IMDEA Software Institute faculty member César Sánchez and obtained his degree from Universidad Politécnica de Madrid with a “cum laude” mention.
