Seminar details
Résumé : Titre : Analyse statique par interprétation abstraite et procédures de décision.
L'interprétation abstraite est une technique classique d'analyse statique qui permet de calculer une sur-approximation des état atteignables d'un programme. Cette sur-approximation peut être rendue plus précise en distinguant tous les chemins à l'intérieur des boucles, mais cette énumération de chemins a un coût exponentiel. L'utilisation de techniques SMT permet d'éviter en général cette énumération exhaustive, et de travailler sur des représentations compactes de ces ensembles de chemins.
L'exposé présente ces techniques combinant interprétation abstraite et SMT-solving, ainsi que l'outil d'analyse PAGAI
