Spécification et vérification de programmes orientés objets en logique de séparation

This thesis develops a verification system in separation logic for multithreaded Java programs. In addition, this thesis shows three new analyses based on separation logic.Separation logic is a variant of linear logic that did a recent breakthrough in program verification. In the literature, separation logic has been applied to simple while programs, while programs with parallelism, and sequential object oriented programs. We complete these works by adapting separation logic to multithreaded object-oriented programs à la Java.To pursue this goal, we develop new verification rules for Java's primitives for multithreading. The basis of our work consists of a model language that we use throughout the thesis. All our formalisation is based on this model language.First, we propose new verification rules for fork and join. Fork starts a new thread while join waits until the receiver thread terminates. Fork and join are used in many mainstream languages including Java, C++, C#, and python. Then, we describe verification rules for reentrant locks i.e. Java's locks. Reentrant locks - as opposed to posix locks - can be acquired multiple times (and released accordingly). This property eases the programmer's task, but it makes verification harder.Second, we present three new analyses based on separation logic. The first analysis completes Cheon et al.'s work on sequences of allowed method calls (i.e. protocols). We extend this work to multithreaded programs and propose a technique to verify that method contracts comply with class protocols. The second analysis permits to show that a separation logic formula does not entail another formula. This algorithm works as follows: given two formulas A and B, the size of A and B's models is approximated; then if the sizes of models are incompatible, the algorithm concludes that A does not entail B. This algorithm is useful in program verifiers, because they have to decide entailment often. The third analysis shows how to parallelize and optimize programs by looking at their proofs in separation logic. This algorithm is implemented in a tool called éterlou.Finally, we conclude and discuss possible future work.Cette thèse propose une extension de la logique de séparation pour les programmes parallèles et orientés-objets. La logique de séparation est un formalisme récent et prometteur pour vérifier les programmes impératifs. Cependant, jusqu'à présent, la logique de séparation a été appliquée à des programmes utilisant un opérateur parallèle irréaliste (||) et des verrous non-ré-entrants (contrairement au langage Java). Dans cette thèse, nous adaptons la logique de séparation aux opérateurs "fork" et "join" (utilisés par de nombreux langages: C, Java, etc...) et aux verrous ré-entrants (utilisés par le langage Java).Cette adaptation inclut un système de vérification pour des programmes similaires aux programmes Java. Ce système est constitué d'un ensemble de triplets de Hoare qui forment un algorithme de vérification. La preuve de correction de ce système a été effectuée et ce système a été évalué sur plusieurs exemples ambitieux (dont la classe Itérateur de la librairie Java et un algorithme de couplage de verrous).En plus de l'extension décrite ci-dessus, plusieurs analyses utilisant la logique de séparation ont été inventées.La première analyse consiste à spécifier les séquences d'appels de méthodes autorisées (appelés "protocoles") dans les classes. Cette analyse décrit finement des protocoles complexes (telle que celui de la classe Itérateur). En outre, nous avons proposé une nouvelle technique permettant de vérifier que les spécifications d'un programme sont correctes en utilisant les protocoles.La seconde analyse permet de montrer qu'une formule en logique de séparation n'implique pas une autre formule. Cela est utile dans les vérificateurs de programmes car ceux-ci doivent fréquemment démontrer des implications entre formules. L'intérêt de cette analyse est que sa complexité est basse : cela permet de l'utiliser souvent sans consommer beaucoup de ressources.La troisième analyse permet de paralléliser automatiquement des programmes. Cette analyse prend en entrée des programmes prouvés en logique de séparation et rend en sortie des programmes parallélisés, optimisés, et prouvés. Notre analyse utilise la sémantique de séparation de l'opérateur "*" pour détecter quand deux sous programmes accèdent à des parties disjointes du tas. Dans ce cas, la parallélisation est possible. L'algorithme de détection est implémenté par un système de réécriture