IPEG

IPEG (Infeasible Path Explanation and Generalization) est un outil d'exécution symbolique dynamique propriétaire développé pour expérimenter la généralisation de chemin infai­sa­ble et ses utilisations. À partir d'un programme écrit dans un sous-ensemble significatif du langage C, IPEG est capable :

• de trouver les chemins infaisables par exécution symbolique ;
• d'analyser la condition de chemin pour expliquer l'infaisabilité de chemin ;
• de généraliser une famille (potentiellement infinie) de chemins infaisables (capturée sous la forme d'un automate) à partir d'un seul chemin infaisable ;
• de combiner les automates de chemins infaisables.

Et, avec ses plus de 10000 lignes de code OCaml et Prolog, IPEG peut, en fin de compte, générer des données de test efficacement en évitant de nombreux chemins infaisables.

IPEG se connecte à tout solveur de contraintes, notamment :

• CEA Colibri, solveur CLP ;
• ECLiPSe IC, solveur CLP ;
• Yices, solveur SMT (via ma propre bibliothèque OCaml) ;
• Microsoft Z3, solveur SMT.

IPEG utilise également les informations statiques calculées par Frama-C, une plateforme libre d'analyse statique.

Données expérimentales

Programmes : git_config, tcas (SIR), gcd, tritype, erfill, bsearch, merge, selection_sort, checkutf8