Pablo Rotondo (LIGM, Université Gustave Eiffel Paris Est)

Dans cet exposé, nous nous interrogeons sur l’effet de réductions sémantiques simples sur des expressions produites par le modèle aléatoire des arbres de recherche binaire (dits BST-like). Ces arbres unaire-binaire sont souvent utilisés dans les benchmarks des outils de vérification, car leur distribution est très facile à implémenter.

Dans un premier temps, nous introduisons ce que nous entendons par expressions et nous nous plaçons dans le cas où il y a un motif absorbant pour un opérateur donné, qui permet de simplifier les expressions tout en préservant leur sémantique. Nous étudions alors la taille moyenne après avoir simplifié au maximum une expression aléatoire de taille n. Nous démontrons qu’il y a 5 régimes différents, selon deux “thresholds” pour la probabilité de l’opérateur absorbant, allant du cas où il n’y a aucune simplification jusqu’à une réduction presque totale.

Travail en commun avec Florent Koechlin.