Avec Radu Iosif, la logique de séparation mise au service de la vérification formelle

« Contrairement au test et au débogage, nous apportons une preuve mathématique qu’un programme fonctionne dans tous les cas de figure possibles. » Radu Iosif se consacre ainsi à la vérification formelle des systèmes informatiques. Actuellement directeur de recherche CNRS au laboratoire VERIMAG, il travaille également à l’automatisation des processus logiques qu’il utilise.

Lors de la conférence CADE 2023 (Conference on automated deduction), Radu Iosif a obtenu le prix Skolem, décerné en hommage au mathématicien et logicien norvégien Thoralf Albert Skolem (1887-1963). Cette récompense de type Test of Time souligne l’influence qu’a eu, au fil des ans, l’article The tree width of separation logic with recursive definitions, présenté à cette conférence en 2013. Radu Iosif l’avait rédigée avec Adam Rogalewicz, de l’université technique de Brno (République tchèque) et Jirí Simácek, qui travaille désormais pour la société Mavenir.

Cet article traite de la logique de séparation. Développée à la toute fin des années 90, elle part de la logique mathématique classique à qui elle retire certaines règles de raisonnement. Elle se débarrasse notamment du principe selon lequel répéter une vérité n’apporte rien de nouveau. Ici, réitérer une information fait apparaître autant de faits distincts, ce qui permet de déployer de la logique sur un ensemble qui a été décomposé en plusieurs parties disjointes.

Les pointeurs sont des outils de programmation courants, qui contiennent l’adressage mémoire d’un élément afin d’accéder directement à son emplacement dans la mémoire. « Ces mécanismes de bas niveau sont utilisés dans la plupart des langages modernes, comme C++, C# ou Java, souligne Radu Iosif. Ils permettent d’organiser les données, d’y accéder plus rapidement et en utilisant moins de mémoire. La logique de séparation fournit des opérateurs syntaxiques qui aident à décrire indépendamment les pointeurs et la structuration des données dans la mémoire. On peut alors raisonner sur un programme en ne s’intéressant qu’aux cellules de mémoire nécessaires à son exécution. »

La preuve du bon fonctionnement d’un programme n’a alors plus à être apportée, à chaque étape de son exécution, sur l’ensemble de la mémoire disponible. Les formules sont ainsi considérablement raccourcies et simplifiées. Bien qu’élégants, ces raisonnements nécessitaient cependant la résolution à la main de certaines parties. Quand Radu Iosif et ses co-auteurs se sont intéressés à la logique de séparation au début des années 2010, ils ont justement travaillé à pousser son automatisation.

Leur article a fourni des processus qui permettent d’automatiser les prises de décision dans n’importe quel fragment de la formule de vérification d’un programme à base de pointeurs. « À partir de cette idée initiale, nous avons transposé le problème dans des aspects de temps et d’espace de plus en plus complexes, poursuit Radu Iosif. Nos résultats ont été intégrés dans différents outils de vérification automatique de preuve, dont la solution populaire CVC4 développée par les universités de Stanford, de New York et de l’Iowa. J’ai d’ailleurs ensuite travaillé avec un collègue de l’université de l’Iowa pour l’intégration d’une version simplifiée de notre algorithme. »

Radu Iosif s’est depuis tourné vers la vérification de systèmes et d’algorithmes distribués, où il utilise toujours la logique de séparation. Il s’intéresse en particulier au cas de la reconfiguration des réseaux, c’est-à-dire quand ils changent de configuration pour rendre plus accessible un nœud qui reçoit un afflux de requêtes. Vérifier des systèmes distribués dont les architectures des réseaux se modifient eux-mêmes pose des défis fascinants, qui pourraient être résolus avec des outils proches de ceux qui ont permis de raisonner sur les pointeurs.