ITS Tools est un model-checker symbolique acceptant en entrée un large éventail de formalismes et vérifiant des propriétés de sûreté, mais aussi des formules LTL et CTL.