Outil dédié à l'analyse et à l'optimisation de modèles de compteurs abstraits utilisés en vérification formelle. Il permet de déterminer des tailles de ensembles concrets à partir de modèles pseudo-booléens, facilitant ainsi la validation de propriétés logiques complexes. Développé dans le cadre du projet BLaSST, il s'intègre dans des workflows de preuve automatisée pour les systèmes critiques.

Outil dédié à la résolution de problèmes de satisfaction de contraintes (CSP) et à la validation de propriétés logiques sur des modèles formels. Il permet d'analyser des systèmes critiques en vérifiant leur cohérence et en générant des contre-exemples ou des preuves de validité. Développé dans le cadre d'un projet de recherche financé par l'ANR, il s'appuie sur des techniques avancées de logique et de satisfiabilité.