Verde est un outil d'Interactive Runtime Verification (i-RV) conçu pour faciliter le débogage interactif de programmes. Il permet de vérifier dynamiquement des propriétés logicielles pendant l'exécution, en combinant des techniques de débogage traditionnel avec des vérifications automatiques. Adapté aux programmes C/C++ et Java, il offre une approche collaborative pour identifier et corriger les erreurs, réduisant ainsi le temps de développement et améliorant la fiabilité des logiciels.

Le projet Residual Runtime Verification with BISM est une implémentation en tant que plugin pour l'outil d'instrumentation Java BISM. Il permet la vérification de propriétés à l'exécution en instrumentant le code pour capturer des événements de programme spécifiques et détecter les exécutions non conformes.

Timbuk est un cadre de vérification régulier basé sur les Automates d'Arbres et les Systèmes de Réécriture de Termes. Il fournit un ensemble de bibliothèques pour créer et manipuler des Automates d'Arbres et des TRS, effectuer une analyse de faisabilité à l'aide de l'Algorithme de Complétion, et calculer des abstractions capables de vérifier des propriétés de sécurité sur des programmes fonctionnels de haut niveau.

Bibliothèque de support pour l'assistant de preuve Coq, fournissant des fichiers vernaculaires pour l'importation des certificats générés par Gappa et un tactic `gappa` pour appeler Gappa sur le but courant dans Coq. Gappa est un outil destiné à aider à la vérification et à la preuve formelle de propriétés sur des programmes numériques utilisant des calculs arithmétiques en virgule flottante ou à point fixe.

Outil d'analyse et de vérification formelle de programmes pour détecter des erreurs logiques, optimiser des blocs de code et valider des propriétés de sécurité. Utilisé principalement dans la recherche académique et l'ingénierie logicielle pour améliorer la fiabilité des systèmes critiques.

Projet open source permettant de transformer du code écrit en WhyML, un langage de spécification et de preuve, en code Java exécutable. Il facilite la vérification formelle de propriétés logiques sur des algorithmes tout en produisant un code source compatible avec l'écosystème Java. Utilisé principalement dans le domaine de la recherche académique et de la validation de programmes.

Gappa est un outil conçu pour aider à la vérification et à la preuve formelle de propriétés sur des programmes numériques traitant des calculs en virgule flottante ou à point fixe.

VeriFast est un outil d'analyse statique formelle conçu pour vérifier la correction de programmes écrits en C et Java. Il permet de détecter des erreurs de typage, des violations de propriétés de sécurité et des bugs potentiels avant l'exécution. Utilisé principalement dans les domaines critiques comme les systèmes embarqués ou les applications sécurisées, il aide les développeurs à prouver que leur code respecte des spécifications formelles.

VeriFast est un outil d'analyse statique conçu pour vérifier la sécurité et la correction des programmes. Il permet de détecter des vulnérabilités potentielles dans le code source, notamment en Java, en s'appuyant sur des annotations et des propriétés formelles. L'outil est utilisé pour garantir la robustesse des systèmes critiques, comme les cartes à puce ou les applications embarquées, en identifiant les erreurs de logique ou les failles de sécurité avant leur déploiement.

Ce projet propose une série d'outils mathématiques et algorithmiques pour résoudre des exercices variés. Il permet de vérifier des propriétés numériques, de décomposer des nombres, de calculer des sommes ou des sous-ensembles, et de manipuler des chaînes de caractères. Idéal pour l'apprentissage ou l'entraînement en mathématiques et en programmation.