Skip to content

Commit

Permalink
add TIS Analyzer FR and EN descriptions
Browse files Browse the repository at this point in the history
  • Loading branch information
RadioPotin committed Sep 2, 2024
1 parent 84a504a commit 517c009
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 2 deletions.
13 changes: 12 additions & 1 deletion content/en/_index.md
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
15 changes: 14 additions & 1 deletion content/fr/_index.md
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down

0 comments on commit 517c009

Please sign in to comment.