Exploration de la scalabilité de LocFaults

A model checker can produce a trace of counterexample, for an erroneous program, which is often long and difficult to understand. In general, the part about the loops is the largest among the instructions in this trace. This makes the location of errors in loops critical, to analyze errors in the overall program. In this paper, we explore the scalability capabilities of LocFaults, our error localization approach exploiting paths of CFG(Control Flow Graph) from a counterexample to calculate the MCDs (Minimal Correction Deviations), and MCSs (Minimal Correction Subsets) from each found MCD. We present the times of our approach on programs with While-loops unfolded b times, and a number of deviated conditions ranging from 0 to n. Our preliminary results show that the times of our approach, constraint-based and flow-driven, are better compared to BugAssist which is based on SAT and transforms the entire program to a Boolean formula, and further the information provided by LocFaults is more expressive for the user.Un vérificateur de modèle peut produire une trace de contre-exemple, pour un programme erroné, qui est souvent longue et difficile a comprendre. En général , la partie qui concerne les boucles est la plus importante parmi les instructions de cette trace. Ce qui rend la localisation d'erreurs dans les boucles cruciale, pour analyser les erreurs dans le programme en global. Dans ce papier, nous explorons les capacités de la scalabilité de LocFaults, notre approche de localisation d'erreurs exploitant les chemins du CFG(Controle Flow Graph) à partir d'un contre-exemple pour calculer les DCMs(Déviations de Correction Minimales), ainsi les MCSs(Minimal Correction Subsets) à partir de chaque DCM. Nous présentons les temps de notre approche sur des programmes avec boucles While dépliées b fois, et un nombre de conditions déviées allant de 0 à n. Nos résultats préliminaires montrent que les temps de notre approche, basée sur les contraintes et dirigée par les flots, sont meilleurs par rapport a BugAssist qui se base sur SAT et transforme la totalité du programme en une formule booléenne , et de plus l'information fournie par LocFaults est plus expressive pour l'utilisateur