Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

Execution Symbolique

No description
by

Riadh Dziri

on 20 December 2013

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Execution Symbolique

Limitations
Tracer exécute tous les chemins possibles du programme mais il ne supporte pas la vérification des grands programmes.
Conclusion
TRACER
PLAN
Introduction
Exécution Symbolique
Étude de cas TRACER
TRACER
Limitations
Conclusion
Principe de Tracer
implémente l’exécution symbolique avec certaines nouvelles fonctionnalités .
Exemple
Introduction
L'exécution symbolique
Un outil pour vérifier les caractéristiques de sécurité des programmes C .
créé par un ensemble des étudiants de l'Université nationale de Singapour
<0> s=0;
<1> if(*)
<2> s++;
else
<3> s+=2;
<4> if(*)
<5> s++;
else
<6> s+=2;
<7> if(s > 10)
<8> error();
<9>
Une technologie permet de couvrir les chemins d'exécution possibles d'un programme et d'analyser dans lequel l'exécution du programme est simulée à l'aide des symboles .
Son but est d'analyser statiquement un programme pour trouver des bugs ou prouver certaines propriétés du programme .
Il prend des entrées symboliques au lieu de données réelles .


Lors de l'exécution d'un chemin de toutes ses contraintes sont accumulées dans une formule logique du premier ordre (FOL) appelée PATH CONDITION (PC).
Le nombre de chemins possibles dans un programme croît de façon exponentielle avec l'augmentation de la taille du programme et peut même être infini dans le cas des programmes avec des itérations de la boucle sans limites ( unbounded loops , récursivité ).
TRACER a déjà prouvé son efficacité dans des essais et trouver des erreurs dans une variété de logiciels mais en raison des limites qu'il possède ,TRACER ne peut pas vérifier symboliquement tout type de programme ce qui permet à des outils qui utilisent des autres approches capables de résoudre ses problèmes.
<0> lock=0; new=old+1;
<1> while(new != old) {
<2> lock=1; old=new;
<3> if(*)
<4> lock=0; new++;
<5> }
<6> if(lock == 0)
<7> error();
<8>
Exemple
Full transcript