Outil académique dédié à la vérification compositionnelle de systèmes temps réel embarqués. Il permet de modéliser des tâches critiques, de générer des problèmes de programmation linéaire en nombres entiers (ILP) pour résoudre des contraintes d'affinité, et de traduire ces descriptions en modèles compatibles avec des outils de vérification formelle comme Uppaal. Utilisé pour des études de cas industrielles, notamment dans le domaine automobile.