Hélène Collavizza

Hélène Collavizza, Claude Michel, Michel Rueher

Programs with floating-point computations are often derived from mathematical models or designed with the semantics of the real numbers in mind. However, for a given input, the computed path with floating-point numbers may differ from the path corresponding to the same computation with real numbers. A common practice when validating such programs consists in estimating the accuracy of floating-point computations with respect to the same sequence of operations in an ide-alized semantics of real numbers. However, state-of-the-art tools compute an over-approximation of the error introduced by floating-point operations. As a consequence, totally inappropriate behaviors of a program may be dreaded but the developer does not know whether these behaviors will actually occur, or not. In this paper, we introduce a new constraint-based approach that searches for test cases in the part of the over-approximation where errors due to floating-point arithmetic would lead to inappropriate behaviors.

Mohammed Bekkouche, Hélène Collavizza, Michel Rueher

In this article, we present our improved algorithm for error localization from counterexamples, LocFaults, flow-driven and constraint-based. This algorithm analyzes the paths of CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of control flow graph for which at most k conditional statements can be wrong. Then we compute the MCSs (Minimal Correction Set) of bounded size on each of these paths. Removal of one of these sets of constraints gives maximal satisfiable subset, in other words, a maximal satisfiable subset satisfying the postcondition. To calculate the MCSs, we extend the generic algorithm proposed by Liffiton and Sakallah in order to deal programs with numerical instructions more effectively. We are interested to present the incremental aspect of this new algorithm that is not yet presented.

Mohammed Bekkouche, Hélène Collavizza, Michel Rueher

We introduce in this paper a new CP-based approach to support errors location in a program for which a counter-example is available, i.e. an instantiation of the input variables that violates the post-condition. To provide helpful information for error location, we generate a constraint system for the paths of the CFG (Control Flow Graph) for which at most k conditional statements may be erroneous. Then, we calculate Minimal Correction Sets (MCS) of bounded size for each of these paths. The removal of one of these sets of constraints yields a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the post condition. We extend the algorithm proposed by Liffiton and Sakallah \cite{LiS08} to handle programs with numerical statements more efficiently. We present preliminary experimental results that are quite encouraging.