diff --git a/content/en/_index.md b/content/en/_index.md index 104983b..827deee 100644 --- a/content/en/_index.md +++ b/content/en/_index.md @@ -114,7 +114,18 @@ software: - name: "TIS Analyzer" url: - "https://www.trust-in-soft.com/trustinsoft-analyzer" - description: "Soon..." + description: + "TrustInSoft Analyzer is a static analyzer for C and C++ code. It + includes several complementary analysis techniques. The first uses + abstract interpretation to verify the absence of undefined behaviors (UB) + in a program. These undefined behaviors can lead to runtime errors and + constitute a large portion of security vulnerabilities in C and C++ + software. The second level of analysis, in addition to verifying the + absence of UB, checks the validity of functional properties expressed as + function contracts and assertions in the code. This part is done by + translating C/C++ code into WhyML via Why3. These analysis techniques are + used in industry and are recognized by the U.S. federal agency, the + National Institute of Standards and Technology (NIST)." collaborators: sectiontitle: "The consortium" diff --git a/content/fr/_index.md b/content/fr/_index.md index 5927081..4a6e6a9 100644 --- a/content/fr/_index.md +++ b/content/fr/_index.md @@ -118,7 +118,20 @@ software: - name: "TIS Analyzer" url: - "https://www.trust-in-soft.com/trustinsoft-analyzer" - description: "Bientôt..." + description: + "TrustInSoft Analyzer est un analyseur statique de code C et C++. Il + comprend plusieurs techniques complémentaires d'analyses. La première + utilise l'interprétation abstraite pour vérifier l'absence de + comportements non-définis (undefined behavior (UB) en anglais) dans un + programme. Ces comportements non-définis peuvent mener à des runtime + errors et constituent une large part des failles de sécurité des + logiciels C et C++. Le deuxième niveau d'analyse permet, en plus de la + vérification de l'absence d'UB, de vérifier la validité de propriétés + fonctionnelles exprimées sous la forme de contrats de fonction et + d'assertions dans le code. Cette partie se fait en traduisant Why3 via + une traduction du code C/C++ en WhyML. Ces techniques d'analyses sont + utilisées industriellement et sont reconnues par l'agence américaine + fédérale National Institute of Standards and Technology (NIST)." collaborators: sectiontitle: "Le consortium"