Encodage de la théorie des ensembles de TLA+ pour la preuve automatique par SMT

March 10, 2025

Rosalie Defourné (IRIT)

Cette présentation résume mes travaux de thèse autour de TLA+ et de son système de preuves. TLA+ est un langage de spécification basé sur la théorie des ensembles non typée. Son prouveur, TLAPS, génère et encode des obligations de preuve pour différents solveurs externes. Je me suis intéressée à l’encodage SMT dans l’optique de le rendre plus sûr d’utilisation, car il est apparu que l’ancienne version contenait des bugs. Je commencerai par exposer les bases de TLA+, puis je décrirai les étapes essentielles de l’encodage. L’innovation principale de ces travaux est le recours aux “triggers” de SMT, qui ont permis d’optimiser l’instanciation au premier ordre et de rendre l’encodage efficace en pratique.