Garantie de déterminisme pour toutes les entrées pour les programmes C
1 : TrustInSoft
TrustInSoft
Des travaux, guidés par le besoin de rendre un analyseur statique de C basé sur l'interprétation abstraite plus utilisable sur les programmes manipulant explicitement la représentation de certaines addresses, ont mené à une définition plus rigoureuse de ce que signifie être déterministe pour un programme C. La nouvelle version de l'analyseur est capable de garantir qu'un programme C est déterministe pour toutes ses entrées, c'est à dire, que pour chaque entrée, il ne peut y avoir qu'un seul résultat calculé.
- Poster