Polyspace Code Prover

Polyspace^®Code Prover™ prouve l'absence d'overflow, de division par zéro, de dépassement de tableaux et de certaines autres erreurs run-time dans du code source C et C++. Il produit des résultats sans nécessité d'exécution du programme, d’instrumentation du code ou de cas de tests. Polyspace Code Prover utilise l’analyse statique et l’interprétation abstraite basées sur des méthodes formelles. Vous pouvez l'utiliser sur du code manuel, du code généré, ou une combinaison des deux. Un code couleur est utilisé pour indiquer si chaque opération est exempte d’erreurs run-time, avérée défaillante, inaccessible ou non prouvée.

Polyspace Code Prover affiche les informations de plage pour les variables et les valeurs renvoyées par les fonctions ; il peut identifier les variables qui dépassent les limites de plage spécifiées. Les résultats peuvent être publiés dans un tableau de bord pour permettre le suivi des métriques de qualité et garantir la conformité avec les objectifs de qualité logicielle.

Le support des normes industrielles est assuré via l'IEC Certification Kit (ISO 26262 and IEC 61508) et le DO Qualification Kit (DO-178).