Up to techniques for bisimulations
Techniques modulo pour les bisimulations
Résumé
While programming languages tend to give higher abstraction levels to the programmer, the programs that are written nowadays tend to be more complex: these programs are distributed, concurrent, interactive, and often, mobile. Moreover the critical role they may play sometimes requires a really precise analysis of their properties. This dissertation is devoted to the study of proof techniques for the analysis of such programs.
We develop a theory of “up-to” techniques for coinduction, in the abstract setting of complete lattices. This theory contains new and general modularity results; it establishes the grounds for the reminder of the dissertation, where we focus on up-to techniques for bisimilarity. Up-to techniques for weak bisimilarity are known to be problematic. We show that these problems are related to similar phenomenons in term rewriting theory, and, using tools from this domain (strong normalisation and well-founded inductions), we develop up-to techniques going beyond existing ones. The benefits of these new tech- niques are illustrated by applying one of them in order to prove the correctness of a non-trivial distributed algorithm, for which standard techniques are not sufficient to give a satisfactory proof.
Independently, by applying our general theory of up-to techniques in the function space, we show how to obtain second-order techniques, that allow us to revisit the “up to context” techniques: we define a generic method that greatly simplifies the study of such techniques. We illustrate this method by using it to recover up to contexts techniques in the case of CCS.
Bien que les langages de programmation actuels fournissent des niveaux d’abstraction de plus en plus élevés, les programmes définis de nos jours sont de plus en plus délicats à étudier : ils sont distribués, concurrents, interactifs, et bien souvent mobiles. De plus, le rôle parfois critique qu’ils endossent nécessite une analyse de plus en plus fine de leurs propriétés. Nous étudions dans cette thèse des techniques de preuve permettant de faciliter l’étude de tels programmes.
Nous développons tout d’abord une théorie des techniques “modulo” pour la coinduction, dans le cadre abstrait des treillis complets. Cette théorie, qui établit des résultats de modularité génériques, fournit un socle solide pour la suite de la thèse, dédiée aux techniques modulo pour la bisimilarité. Dans le cas dit “faible” ces techniques modulo souffrent de limitations, dues à des phénomènes bien connus en théorie de la réécriture. En utilisant les outils de ce domaine (normalisation forte et inductions bien fondées), nous définissons de nouvelles techniques afin de contourner ces limitations. L’utilité de ces techniques est illustrée par l’étude détaillée d’un algorithme distribué non trivial (il s’agit de l’optimisation d’un environnement d’exécution pour des processus distribués), et pour lequel les techniques standard s’avèrent insuffisantes
D’autre part, en appliquant notre théorie des techniques modulo dans un espace de fonctions, nous montrons comment obtenir des techniques de second ordre, qui nous per- mettent de revisiter les techniques dites “modulo contexte” : nous définissons une méthode qui permet de simplifier grandement l’étude de telles techniques, en la ramenant de façon systématique à une étude de cas élémentaire. Nous illustrons cette méthode en l’appliquant dans le cas de CCS.