Ce projet vise à fournir une preuve formelle de la sécurité des systèmes informatiques en utilisant la logique de séparation avec crédits de temps. Il permet de vérifier des propriétés temporelles dans des programmes concurrents et de développer des spécifications formelles pour des systèmes temps-réel.