Démonstration de Steel, une logique de séparation concurrente pour prouver des programmes F* (démonstration)

National audience; Steel est un framework pour développer et prouver des programmes concurrents écrits en F , un langage de programmation avec types dépendants ainsi qu'un assistant de preuve. Inspiré par Iris, Steel repose sur une logique de séparation concurrente imprédicative qui inclut un modèle mémoire fondé sur des monoïdes commutatifs partiels et permet l'utilisation d'invariants alloués dynamiquement pour raisonner sur des interactions concurrentes sans recourir à des verrous ("locks"). Afin d'offrir une vérification semi-automatique, Steel sépare les obligations de preuves générées en deux parties : une procédure de décision partielle, implémentée à l'aide du moteur de tactiques de F , raisonne sur la logique de séparation tandis qu'un solveur SMT permet de décharger automatiquement des obligations de preuves exprimées en logique du premier ordre, par exemple liées à de l'arithmétique. Dans cette démonstration, nous présentons plusieurs bibliothèques vérifiées qui illustrent l'expressivité et la programmabilité de Steel.