PRISM est un outil open source dédié à la vérification formelle de systèmes probabilistes et stochastiques. Il permet de modéliser et d'analyser des systèmes complexes comme les protocoles de communication, les algorithmes distribués ou les réseaux de files d'attente. L'outil prend en charge plusieurs formalismes (DTMC, CTMC, MDP, etc.) et offre des fonctionnalités avancées pour l'évaluation de propriétés quantitatives et temporelles.

Projet académique visant à analyser et comparer les performances et la sécurité des algorithmes cryptographiques face aux attaques par canaux auxiliaires. Il propose des outils pour évaluer les fuites temporelles et valider des propriétés de mémoire constante, notamment via des modes sécurisés (exposé, verrouillé, sans branchement, etc.). Les résultats sont générés sous forme de fichiers CSV pour faciliter l'analyse comparative.