De façon très schématique on établit des correspondances entre les composants du langage
source et des opérations mathématiques qui permettent de garantir une évaluation d'un graphe
associé à celui du programme en une durée limitée.
Suivant la correspondance choisie, on obtient des indications sur tel ou tel type de propriétés du code.
Après c'est Google/Cousot.
Les articles de 76 sont accessibles avec un bagage mathématique minimal (interdit aux moins de 16 ans :o) ).
[^] # Re: Buffer overflows ...
Posté par François Romieu . En réponse à la dépêche MicroBSD. Évalué à 4.
source et des opérations mathématiques qui permettent de garantir une évaluation d'un graphe
associé à celui du programme en une durée limitée.
Suivant la correspondance choisie, on obtient des indications sur tel ou tel type de propriétés du code.
Après c'est Google/Cousot.
Les articles de 76 sont accessibles avec un bagage mathématique minimal (interdit aux moins de 16 ans :o) ).
--
Ueimor