=Paper=
{{Paper
|id=Vol-3642/paper1
|storemode=property
|title=Locating Loop Errors in Programs: A Scalable and Expressive Approach using LocFaults
          
|pdfUrl=https://ceur-ws.org/Vol-3642/paper1.pdf
|volume=Vol-3642
|authors=Mohammed Bekkouche
|dblpUrl=https://dblp.org/rec/conf/tacc/Bekkouche23
}}
==Locating Loop Errors in Programs: A Scalable and Expressive Approach using LocFaults
          ==
<pdf width="1500px">https://ceur-ws.org/Vol-3642/paper1.pdf</pdf>
<pre>
                                Locating Loop Errors in Programs: A Scalable and
                                Expressive Approach using LocFaults
                                Mohammed Bekkouche1,*
                                1
                                    LabRI-SBA Laboratory, École Supérieure en Informatique, Sidi Bel Abbes 22000, Algeria


                                                                         Abstract
                                                                         A model checker can generate a lengthy and complicated trace of counterexamples for an erroneous
                                                                         program, with the loop instructions being the largest part of this trace. Consequently, the location of
                                                                         errors in loops is critical to analyzing the overall program. In this paper, we delve into the scalability
                                                                         potential of LocFaults, our error localization approach that utilizes Control Flow Graph (CFG) paths
                                                                         from counterexamples to calculate the Minimal Correction Deviations (MCDs) and Minimal Correction
                                                                         Subsets (MCSs) for each MCD found. The study presents the efficiency of LocFaults on programs with
                                                                         While-loops unfolded b times and deviated conditions ranging from 0 to n. Preliminary results show
                                                                         that LocFaults, constraint-based and flow-driven, is faster and provides more expressive information
                                                                         for the user compared to BugAssist, which is based on SAT and transforms the entire program into a
                                                                         Boolean formula.

                                                                         Keywords
                                                                         Error localization, LocFaults, BugAssist, Off-by-one bug, Minimal Correction Deviations, Minimal
                                                                         Correction Subsets




                                1. Introduction
                                Errors are inevitable in a program; they can disrupt proper operation and lead to serious finan-
                                cial consequences, posing a threat to human well-being [1]. Some software bug stories are cited
                                in this link [2]. Consequently, the debugging process, which involves detecting, localizing, and
                                correcting errors, is essential. Localizing errors is the most costly step, requiring the identifi-
                                cation of the precise locations of suspicious instructions [3] to help the user understand why
                                the program failed and facilitate error correction. When a program 𝑃 does not conform to its
                                specification (i.e., contains errors), a model checker can produce a trace of a counterexample,
                                which is often long and challenging to comprehend, even for experienced programmers. To
                                address this issue, we have proposed an approach named LocFaults [4], which is based on
                                constraints that explore the paths of the program’s Control Flow Graph (CFG) from the coun-
                                terexample to calculate the minimal subsets necessary to restore the program’s compliance with
                                its postcondition. Ensuring that our method is highly scalable to meet the enormous complexity
                                of software systems is a crucial criterion for its quality [5].

                                TACC 2023: Tunisian-Algerian Joint Conference on Applied Computing, November 06–08, 2023, Sousse, Tunisia
                                *
                                 Corresponding author.
                                $ m.bekkouche@esi-sba.dz (M. Bekkouche)
                                € https://www.esi-sba.dz/fr/index.php/personnel/bekkouche-mohammed/ (M. Bekkouche)
                                 0000-0002-8305-0542 (M. Bekkouche)
                                                                       © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
                                    CEUR
                                    Workshop
                                    Proceedings
                                                  http://ceur-ws.org
                                                  ISSN 1613-0073
                                                                       CEUR Workshop Proceedings (CEUR-WS.org)




CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
   Several statistical approaches for error localization have been proposed, such as Tarantula [6,
7], Ochiai [8], AMPLE [8], Pinpoint [9], FLCN-S [10], FTFL [11], ConsilientSFL [12], and
Poster [13]. Among them, Tarantula is the most famous and uses different metrics to calculate
the degree of suspicion of each instruction in the program while running a series of tests.
However, these approaches have a drawback in that they require a large number of test cases,
while our approach only uses one counterexample. Another challenge with statistical approaches
is the need for an oracle to determine if a test case’s result is correct or not. To address this issue,
we utilize the Bounded Model Checking (BMC) framework, which only requires a postcondition
or assertion to verify.
   Our approach aims to simplify the problem of error localization by reducing it to computing
a minimal set that explains why a Constraint Satisfaction Problem (CSP) is infeasible. The CSP
represents the constraints of the program, counterexample, and the assertion or postcondition
violated. The calculated set can be either a Minimal Correction Subset (MCS) or a Minimal
Unsatisfiable Subset (MUS). Generally, testing the feasibility of a CSP over a finite domain is an
NP-complete problem, which is one of the most difficult NP problems. Thus, explaining the
infeasibility in a CSP is equally challenging, if not harder, and can be classified as an NP-hard
problem. While BugAssist [14, 15] is a BMC-based error localization method that employs a
Max-SAT solver to compute the merger of MCSs of the Boolean formula of the entire program
with the counterexample, it becomes inefficient for large programs. LocFaults also works from
a counterexample to calculate MCSs.
   In this paper, we investigate the scalability of LocFaults on programs with While-loops that
are unfolded b times, and a number of deviated conditions ranging from 0 to 3. Our approach
contributes in the following ways compared to BugAssist:

    • We avoid transforming the entire program into a system of constraints. Instead, we use the
      CFG (Control Flow Graph) of the program to gather the constraints of the counterexample
      path and paths derived from it. We assume that at most k conditionals may contain errors,
      and we calculate MCSs only on the counterexample path and paths that correct the
      program.
    • We do not convert program instructions into a SAT (Boolean satisfiability) formula.
      Instead, we use numerical constraints that will be handled by constraint solvers.
    • We do not rely on MaxSAT solvers as black boxes. Instead, we use a generic algorithm
      that uses a constraint solver to calculate MCSs.
    • We limit the size of the generated MCSs and the number of deviated conditions.
    • We can work together multiple solvers during the localization process and choose the
      most efficient one according to the category of the CSP (Constraint Satisfaction Problem)
      constructed. For example, if the CSP of the detected path is linear over integers, we use
      a MIP (Mixed Integer Programming) solver. If it is nonlinear, we use a CP (Constraint
      Programming) and/or MINLP (Mixed Integer Nonlinear Programming) solver.

  Based on our practical experience, as demonstrated in Section 5, we have found that the
restrictions and distinctions employed by LocFaults make it faster and more expressive.
  The paper is organized as follows. Section 2 introduces the definition of MUS and MCS. In
Section 3, we define the ≤ k-MCD problem. In section 4, we describe our contribution to treating
erroneous loops, including the Off-by-one bug. The results of our experimental evaluation are
presented in Section 5. Section 6 includes the conclusion and discussion of future work.


2. Definitions
In this section, we introduce the definition of an IIS/MUS and MCS.

CSP. A CSP (Constraint Satisfaction Problem) 𝑃 is defined as a triple < 𝑋, 𝐶, 𝐷 >, where:
    • 𝑋 : a set of 𝑛 variables 𝑥1 , 𝑥2 , ..., 𝑥𝑛 .
    • 𝐶 = {𝑐1 , 𝑐2 , ..., 𝑐𝑚 } is the set of constraints.
    • 𝐷 : the tuple < 𝐷𝑥1 , 𝐷𝑥2 , ..., 𝐷𝑥𝑛 >. The set 𝐷𝑥𝑖 contains the values of the variable 𝑥𝑖 .
  A solution for 𝑃 is an instantiation of the variables 𝐼 ∈ 𝐷 that satisfies all the constraints in
𝐶. 𝑃 is infeasible if it has no solutions. A sub-set of constraints 𝐶 ′ in 𝐶 is also said infeasible
for the same reason except that it is limited to the constraints in 𝐶 ′ .
  We denote as:
    • 𝑆𝑜𝑙(< 𝑋, 𝐶 ′ , 𝐷 >) = ∅, to specify that 𝐶 ′ has no solutions, so it is infeasible.
    • 𝑆𝑜𝑙(< 𝑋, 𝐶 ′ , 𝐷 >) ̸= ∅, to specify that 𝐶 ′ has at least one solution, so it is feasible.
   A Linear Program, denoted as LP, is said to be linear if all the constraints in the set 𝐶 are
expressed as linear equations or inequalities. It is considered continuous if the domain of all
variables is real. If at least one variable in the set 𝑋 is an integer or a binary (which is a special
case of an integer), and the constraints are linear, then 𝑃 is referred to as a Mixed-Integer Linear
Program (MIP). If the constraints are expressed as nonlinear equations or inequalities, then 𝑃 is
referred to as a Nonlinear Program (NLP).
   Let 𝑃 =< 𝑋, 𝐶, 𝐷 > an infeasible CSP, we define for 𝑃 :

IS. An IS (Inconsistent Set) is an infeasible subset of constraints in the constraint set infeasible
𝐶. 𝐶 ′ is an IS iff:
    • 𝐶 ′ ⊆ 𝐶.
    • 𝑆𝑜𝑙(< 𝑋, 𝐶 ′ , 𝐷 >) = ∅.

IIS or MUS. An IIS (Irreducible Inconsistent Set) or MUS (Minimal Unsatisfiable Subset) is an
infeasible subset of constraints of 𝐶, and all its strict subsets are feasible. 𝐶 ′ is an IIS iff :
    • 𝐶 ′ is an IS.
    • ∀𝐶 ′′ ⊂ 𝐶 ′ .𝑆𝑜𝑙(< 𝑋, 𝐶 ′′ , 𝐷 >) ̸= ∅, (each of its parts contributes to the infeasibility), 𝐶 ′
      is called irreducible.

MCS.     𝐶 ′ is a MCS (Minimal Correction Set) iff :
    • 𝐶 ′ ⊆ 𝐶.
    • 𝑆𝑜𝑙(< 𝑋, 𝐶∖𝐶 ′ , 𝐷 >) ̸= ∅.
    • ∄ 𝐶 ′′ ⊂ 𝐶 ′ such as 𝑆𝑜𝑙(< 𝑋, 𝐶∖𝐶 ′′ , 𝐷 >) = ∅.
3. The problem ≤ k-MCD
Given an erroneous program modeled in a CFG1 𝐺 = (𝐶, 𝐴, 𝐸), where 𝐶 is the set of conditional
nodes, 𝐴 is the set of assignment blocks, and 𝐸 is the set of arcs, along with a counterexample, a
Minimal Correction Deviation (MCD) is a set 𝐷 ⊆ 𝐶 such that propagating the counterexample
on all the instructions of 𝐺 from the root, while having negated each condition2 in 𝐷, allows
the output to satisfy the postcondition. A MCD is called minimal (or irreducible) if no element
can be removed from 𝐷 without losing this property. In other words, 𝐷 is a minimal program
correctness in the set of conditions. The size of the minimal deviation is its cardinality. The
problem of finding all MCDs of size smaller or equal to 𝑘 is denoted as ≤ k-MCD.
  As an illustration (refer to Fig. 1), consider the CFG of the program AbsMinus (refer to
Fig. 1b). When provided with the counterexample {𝑖 = 0, 𝑗 = 1}, this program has one
minimal deviation of size 1. While the deviation {𝑖0 ≤ 𝑗0 , 𝑘1 = 1 ∧ 𝑖0 ̸= 𝑗0 } does correct the
program, it is not minimal. In fact, the only minimal correction deviation for this program is
{𝑘1 = 1 ∧ 𝑖0 ̸= 𝑗0 }.

Table 1
The progress of LocFaults for the program AbsMinus
                      Deviated conditions        MCD             MCS              Figure
                               ∅                   /      {𝑟1 = 𝑖0 − 𝑗0 : 13}    Fig. 1c
                          {𝑖0 ≤ 𝑗0 : 8}           No               /             Fig. 1d
                                                             {𝑘0 = 0 : 7},
                   {𝑘1 = 1 ∧ 𝑖0 ! = 𝑗0 : 10}      Yes                             Fig. 1e
                                                           {𝑘1 = 𝑘0 + 2 : 9}
                         {𝑖0 ≤ 𝑗0 : 8,
                                                  No                /             Fig. 1f
                    𝑘1 = 1 ∧ 𝑖0 ! = 𝑗0 : 10}

   Table 1 provides a summary of the progress of LocFaults for the program AbsMinus, with
at most 2 conditions deviated from the counterexample {𝑖 = 0, 𝑗 = 1}. The table displays
the conditions deviated, indicating whether they are minimal or non-minimal deviations, and
the MCSs (Minimal Correction Sets) calculated from the constructed constraint system : see
columns 1, 2, and 3, respectively. Column 4 shows the figure that illustrates the path explored
for each deviation. Additionally, the first and the third columns show the instruction and its
corresponding line in the program.
   For example, the first line in the table indicates that a single MCS ({𝑟1 = 𝑖0 − 𝑗0 : 13}) was
found on the path of the counterexample.


4. Error localization in loops
In the context of Bounded Model Checking (BMC) for programs, unfolding can be applied to the
entire program or to loops separately [5]. Our algorithm, LocFaults [4], for error localization

1
  We use Dynamic Single Assignment (DSA) form [16] transformation that ensures that each variable is assigned
  only once on each path of the CFG.
2
  To navigate to the intended branch, we negate the condition to take the opposite branch.
                                                                                     𝑘0 = 0                                                             𝑘0 = 0

1 class AbsMinus {
2    /*@ ensures
3    @ ((i < j) ==> (\result == j-i
          )) &&                                                                       𝑖0 ≤                                                                𝑖0 ≤
                                                                                       𝑗0                                                                  𝑗0
4    @ ((i >= j) ==> (\result == i-                                            If               Else                                             If                 Else
          j)); */
5    int AbsMinus (int i, int j) {                          𝑘1 = 𝑘0 + 2                                𝑘1 = 𝑘0             𝑘1 = 𝑘0 + 2                                     𝑘1 = 𝑘0
6     int result;
7     int k = 0;
8     if (i <= j) {                                                                   𝑘1 =                                                                𝑘1 =
                                                                                      1 &&                                                                1 &&
9      k = k+2; } // error : k = k                                                    𝑖0 ! =                                                              𝑖0 ! =
            +2 instead of k=k+1                                           If           𝑗0             Else                                  If             𝑗0           Else
10    if (k == 1 && i != j) {
11     result = j-i; }                                     𝑟1 = 𝑗0 − 𝑖0                                 𝑟1 = 𝑖0 − 𝑗0     𝑟1 = 𝑗0 − 𝑖0                                      𝑟1 = 𝑖0 − 𝑗0
12    else {
13     result = i-j; }                                               POST:{𝑟1 = |𝑖0 − 𝑗0 |}                                            POST:{𝑟1 = |𝑖0 − 𝑗0 |}
14    return result; } }
                                                          (b) The CFG in DSA form of Ab- (c) The path of the counterexam-
      (a) The program AbsMinus                                sMinus                         ple
                          𝑘0 = 0                                                    𝑘0 = 0                                                            𝑘0 = 0




                           𝑖0 ≤                                                      𝑖0 ≤                                                              𝑖0 ≤
                            𝑗0                                                        𝑗0                                                                𝑗0
                     If             Else                                  If                   Else                                    If                        Else


      𝑘1 = 𝑘0 + 2                      𝑘1 = 𝑘0             𝑘1 = 𝑘0 + 2                            𝑘1 = 𝑘0               𝑘1 = 𝑘0 + 2                                 𝑘1 = 𝑘0



                           𝑘1 =                                                      𝑘1 =                                                              𝑘1 =
                           1 &&                                                      1 &&                                                              1 &&
                           𝑖0 ! =                                                    𝑖0 ! =                                                            𝑖0 ! =
                If          𝑗0        Else                           If               𝑗0         Else                             If                    𝑗0          else


     𝑟1 = 𝑗0 − 𝑖0                          𝑟1 = 𝑖0 − 𝑗0   𝑟1 = 𝑗0 − 𝑖0                                𝑟1 = 𝑖0 − 𝑗0     𝑟1 = 𝑗0 − 𝑖0                                     𝑟1 = 𝑖0 − 𝑗0


                        POST:{𝑟1 =                                           POST:{𝑟1 =                                                   POST:{𝑟1 =
                    |𝑖0 − 𝑗0 |} is UNSAT                                  |𝑖0 − 𝑗0 |} is SAT                                           |𝑖0 − 𝑗0 |} is SAT


 (d) The path obtained by deviat- (e) The path by deviating the con- (f) The path of a non-minimal de-
     ing the condition 𝑖0 ≤ 𝑗0        dition 𝑘1 = 1 ∧ 𝑖0 ! = 𝑗0          viation
Figure 1: The exploration of AbsMinus CFG performed by LocFaults


follows the latter approach, where we use a bound 𝑏 to unfold loops by replacing them with
nested conditional statements of depth 𝑏. For example, consider the program Minimum (refer to
Fig. 2), which contains a single loop that calculates the minimum value in an array of integers.
The effect on the control flow graph of the program Minimum before and after unfolding is
illustrated in Figures 2 and 3, respectively. The while-loop is unfolded three times, since three
iterations are required to calculate the minimum value for an array of size 4.
   LocFaults takes the CFG of the erroneous program, 𝐶𝐸 (a counterexample), 𝑏𝑚𝑐𝑑 (a bound
on the number of deviated conditions), and 𝑏𝑚𝑐𝑠 (a bound on the size of calculated MCSs) as
input. It enables us to explore the CFG in depth by diverting a maximum of 𝑏𝑚𝑐𝑑 conditions
from the counterexample’s path by performing the following steps:

       • Propagating CE on the CFG until the postcondition is reached. Then, it calculates the
                                                                                                                                                                                                                                                                                           𝑚𝑖𝑛 = 𝑡𝑎𝑏[0]
        1 class Minimum {
                                                                                                                                                                                                                                                                                              𝑖=1
        2 /*The minimum in an array of n integers
                                                                       */
        3 /*@ ensures
        4                                                           @ (\forall int k;(k>=0 && k<tab.
                                                                                                                                                                                                                                                                                                𝑖 <
                                                                         length) ; tab[k]>=min);                                                                                                                                                                                           𝑡𝑎𝑏.𝑙𝑒𝑛𝑔𝑡ℎ −
        5                                                           @*/                                                                                                                                                                                                                          1
        6                                                           int Minimum(int[] tab){
        7                                                             int min=tab[0];                                                                                                                                                                                                If
        8                                                             int i=1;
        9                                                             while(i<tab.length-1){ /*error, the
                                                                            condition should be (i<tab.
                                                                           length)*/                                                                                                                                                                                  Goto                 𝑡𝑎𝑏[𝑖] < 𝑚𝑖𝑛
10                                                                      if(tab[i]<min){                                                                                                                                                                                                                                                                                            Else
11                                                                        min=tab[i];                                                                                                                                                                                                     If

12                                                                      }                                                                                                                                                                                                                                                                                 Else
13                                                                      i=i+1;                                                                                                                                                                                                              𝑚𝑖𝑛 = 𝑡𝑎𝑏[𝑖]
14                                                                    }
15                                                                    return min;                                                                                                                                                                                                                   𝑖=𝑖+1
16                                                                  }
17 }
                                                                                                                                                                                                                                                                                           Postcondition


Figure 2: The program Minimum and its normal CFG (non-unfolded). The postcondition is {∀ int
𝑘; (𝑘 ≥ 0 ∧ 𝑘 < 𝑡𝑎𝑏.𝑙𝑒𝑛𝑔𝑡ℎ); 𝑡𝑎𝑏[𝑘] ≥ 𝑚𝑖𝑛}


                                                                      MCSs on the CSP of the generated path to locate errors on the counterexample’s path.
                                                                    • Seeking to enumerate the sets ≤ 𝑏𝑚𝑐𝑑 − 𝑀 𝐶𝐷. For each found MCD, it calculates the
                                                                      MCSs on the path that reaches the last deviated condition and allows for taking the path
                                                                      of the deviation.
                                                                                                                𝑚𝑖𝑛4 = 𝑚𝑖𝑛0




                                                                                                                                                                                                              𝑚𝑖𝑛4 = 𝑚𝑖𝑛1




                                                                                                                                                                                                                                                                                                                           𝑚𝑖𝑛4 = 𝑚𝑖𝑛2
                                                                                                                                                    𝑚𝑖𝑛1 = 𝑚𝑖𝑛0




                                                                                                                                                                                                                                                  𝑚𝑖𝑛2 = 𝑚𝑖𝑛1




                                                                                                                                                                                                                                                                                                                                                               𝑚𝑖𝑛3 = 𝑚𝑖𝑛2




                                                                                                                                                                                                                                                                                                                                                                                                               POST:{∀ int 𝑘; (𝑘 ≥ 0 ∧ 𝑘 < 𝑡𝑎𝑏0 .𝑙𝑒𝑛𝑔𝑡ℎ);
                                                                                                                  𝑖4 = 𝑖0




                                                                                                                                                                                                                𝑖4 = 𝑖1




                                                                                                                                                                                                                                                                                                                             𝑖4 = 𝑖2
𝐶𝐸 : {𝑡𝑎𝑏0 [0] = 3 ∧ 𝑡𝑎𝑏0 [1] = 2




                                                                                                        Else




                                                                                                                                                                                                      Else




                                                                                                                                                                                                                                                                                                    Else
                                                                                                                                             Else




                                                                                                                                                                                                                                           Else




                                                                                                                                                                                                                                                                                                                                                        Else
                                    ∧𝑡𝑎𝑏0 [2] = 1 ∧ 𝑡𝑎𝑏0 [3] = 0}




                                                                                                                                                                                                                                                                                                                                                                                                                                                            𝑡𝑎𝑏0 [𝑘] ≥ 𝑚𝑖𝑛4 }
                                                                      𝑚𝑖𝑛0 = 𝑡𝑎𝑏0 [0]




                                                                                        𝑡𝑎𝑏0 .𝑙𝑒𝑛𝑔𝑡ℎ−




                                                                                                                                                                                      𝑡𝑎𝑏0 .𝑙𝑒𝑛𝑔𝑡ℎ−




                                                                                                                                                                                                                                                                                    𝑡𝑎𝑏0 .𝑙𝑒𝑛𝑔𝑡ℎ−




                                                                                                                                                                                                                                                                                                                                                                                                 𝑚𝑖𝑛4 = 𝑚𝑖𝑛3
                                                                                                                                                                        𝑖1 = 𝑖0 + 1




                                                                                                                                                                                                                                                                      𝑖2 = 𝑖1 + 1




                                                                                                                                                                                                                                                                                                                                                                                   𝑖3 = 𝑖2 + 1
                                                                                                                              𝑡𝑎𝑏0 [𝑖0 ] <




                                                                                                                                                                                                                            𝑡𝑎𝑏0 [𝑖1 ] <




                                                                                                                                                                                                                                                                                                                                         𝑡𝑎𝑏0 [𝑖2 ] <




                                                                                                                                                                                                                                                                                                                                                                                                   𝑖4 = 𝑖3
                                                                         𝑖0 = 1




                                                                                                                                                                                                                              𝑚𝑖𝑛1
                                                                                                                                𝑚𝑖𝑛0




                                                                                                                                                                                                                                                                                                                                           𝑚𝑖𝑛2
                                                                                            𝑖0 <




                                                                                                                                                                                          𝑖1 <




                                                                                                                                                                                                                                                                                        𝑖2 <
                                                                                               1




                                                                                                                                                                                             1




                                                                                                                                                                                                                                                                                           1
                                                                                                               If




                                                                                                                                                                                                             If




                                                                                                                                                                                                                                                                                                           If(deviation)
                                                                                                                                                    𝑚𝑖𝑛1 = 𝑡𝑎𝑏0 [𝑖0 ]




                                                                                                                                                                                                                                                  𝑚𝑖𝑛2 = 𝑡𝑎𝑏0 [𝑖1 ]




                                                                                                                                                                                                                                                                                                                                                               𝑚𝑖𝑛3 = 𝑡𝑎𝑏0 [𝑖2 ]
                                                                                                                                             If




                                                                                                                                                                                                                                           If




                                                                                                                                                                                                                                                                                                                                                        If




Figure 3: The CFG in DSA form of the program Minimum after unfolding its loop three times, with a
highlighted path of a counterexample in dashed lines and a deviation that satisfies the postcondition in
dotted lines.


  Off-by-one bugs are among the most common errors associated with loops. These bugs
cause loops to iterate one too many or one too few times. The cause of these bugs can be
traced back to improper initialization of loop control variables or an erroneous loop condition.
The program Minimum provides an example of this type of error. The error occurs due to
a falsified instruction in the loop condition (line 9) of the While loop. The correct condition
should be (i < tab.length), where tab.length is the number of elements in the table tab. Using
the counterexample {𝑡𝑎𝑏[0] = 3, 𝑡𝑎𝑏[1] = 2, 𝑡𝑎𝑏[2] = 1, 𝑡𝑎𝑏[3] = 0}, we illustrated the initial
faulty path in Figure 3 (shown in dashed lines) and the deviation for which the postcondition is
satisfiable (the deviation and the path beyond the deviated condition are displayed in dotted
lines).
   Table 2 shows the erroneous paths generated (column PATH) and the corresponding MCSs
calculated (column MCSs) for at most one deviated condition from the execution of the coun-
terexample. The first row pertains to the path of the counterexample, while the second row
corresponds to the path obtained by deviating the condition {𝑖2 ≤ 𝑡𝑎𝑏0 .𝑙𝑒𝑛𝑔𝑡ℎ − 1}.
   LocFaults identifies a single MCS on the path of the counterexample that includes the con-
straint 𝑚𝑖𝑛2 = 𝑡𝑎𝑏0 [𝑖1 ]. This constraint arises from the instruction on line 11 in the second
iteration of the unfolded loop. When a condition is deviated, the algorithm suspects the third
condition of the unfolded loop, i.e., 𝑖2 < 𝑡𝑎𝑏0 .𝑙𝑒𝑛𝑔𝑡ℎ − 1. This deviation implies that we need
to execute a new iteration to satisfy the postcondition.

Table 2
Paths and MCSs generated by LocFaults for the program Minimum
                                           PATH                                                 MCSs
            {𝐶𝐸 : [𝑡𝑎𝑏0 [0] = 3 ∧ 𝑡𝑎𝑏0 [1] = 2 ∧ 𝑡𝑎𝑏0 [2] = 1 ∧ 𝑡𝑎𝑏0 [3] = 0],
        𝑚𝑖𝑛0 = 𝑡𝑎𝑏0 [0], 𝑖0 = 1, 𝑚𝑖𝑛1 = 𝑡𝑎𝑏0 [𝑖0 ], 𝑖1 = 𝑖0 + 1, 𝑚𝑖𝑛2 = 𝑡𝑎𝑏0 [𝑖1 ],
                                                                                         {𝑚𝑖𝑛2 = 𝑡𝑎𝑏0 [𝑖1 ]}
           𝑖2 = 𝑖1 + 1, 𝑚𝑖𝑛4 = 𝑚𝑖𝑛2 , 𝑖4 = 𝑖2 , 𝑃 𝑂𝑆𝑇 : [(𝑡𝑎𝑏0 [0] ≥ 𝑚𝑖𝑛4 )
             ∧(𝑡𝑎𝑏0 [1] ≥ 𝑚𝑖𝑛4 ) ∧ (𝑡𝑎𝑏0 [2] ≥ 𝑚𝑖𝑛4 ) ∧ (𝑡𝑎𝑏0 [3] ≥ 𝑚𝑖𝑛4 )]
            {𝐶𝐸 : [𝑡𝑎𝑏0 [0] = 3 ∧ 𝑡𝑎𝑏0 [1] = 2 ∧ 𝑡𝑎𝑏0 [2] = 1 ∧ 𝑡𝑎𝑏0 [3] = 0],               {𝑖0 = 1},
                𝑚𝑖𝑛0 = 𝑡𝑎𝑏0 [0], 𝑖0 = 1, 𝑚𝑖𝑛1 = 𝑡𝑎𝑏0 [𝑖0 ], 𝑖1 = 𝑖0 + 1,                   {𝑖1 = 𝑖0 + 1},
               𝑚𝑖𝑛2 = 𝑡𝑎𝑏0 [𝑖1 ], 𝑖2 = 𝑖1 + 1, [¬(𝑖2 ≤ 𝑡𝑎𝑏0 .𝑙𝑒𝑛𝑔𝑡ℎ − 1)]                  {𝑖2 = 𝑖1 + 1}

   This example illustrates a case of a program with an incorrect loop. The error lies in the
stopping criterion, which prevents the program from iterating until the last element of the input
array. LocFaults, with its deviation mechanism, is capable of accurately locating this type of
error. It not only identifies suspicious instructions in the unfolded loop that were not present in
the original program, but also provides information about the iterations in which they occur.
This information could be extremely useful for programmers to identify errors in the loop.


5. Practical experience
To evaluate the scalability of our method, we compared its performance with that of BugAssist3
using a benchmark set that we created4 . The benchmark set comprises various implementations


3
    The tool BugAssist can be accessed at http://bugassist.mpi-sws.org/.
4
    The source code for all programs is available at http://capv.toile-libre.org/Benchs_Mohammed.html
of BubbleSort, Sum, and SquareRoot programs, consisting of 19, 48, and 91 variations, respec-
tively. These programs incorporate loops, enabling us to study the scalability of our approach
compared to BugAssist. To increase the program’s complexity, we augmented the number of
loop iterations in the execution of each tool. Both LocFaults and BugAssist were subjected to
the same bound of unfolding loops.
   To generate the CFG and counterexample, we employed the tool CPBPV [17], which stands
for Constraint-Programming Framework for Bounded Program Verification. LocFaults and
BugAssist are designed to operate on Java and C programs, respectively. To enable a fair
comparison, we created two equivalent versions for each program:

       • one version annotated with a JML specification in Java,
       • another version annotated with the same specification in ACSL, using ANSI-C.

Both versions consist of an identical number of lines of instructions, including errors. The
precondition defines the counterexample used for the program.
   For computing the MCSs, we employed the CPLEX solvers of IBM ILOG, encompassing both
MIP and CP solvers. We have implemented the algorithm proposed by Liffiton and Sakallah [18].
This implementation requires as input the infeasible set of constraints that correspond to the
identified path and a bound on the size of calculated MCSs.
   BugAssist leverages the CBMC tool [19] to generate erroneous traces and input data. We
utilized MSUnCore2 [20] as the Max-SAT solver (used by BugAssist).
   The experiments were conducted on an Intel Core i7-3720QM 2.60 GHz processor with 8 GB
of RAM.

5.1. Benchmarks with loops
These benchmarks are utilized to evaluate the scalability of LocFaults in comparison to BugAssist
for programs with loops, based on the increase of unfolding 𝑏. We selected three programs with
loops: BubbleSort, Sum, and SquareRoot, and introduced an Off-by-one bug in each of them.
The benchmark for each program is generated by increasing the number of unfolding 𝑏, where
𝑏 represents the number of iterations through the loop in the worst case. Additionally, we vary
the number of deviated conditions for LocFaults from 0 to 3.
   We utilized the MIP solver of CPLEX for BubbleSort. For Sum and SquareRoot, we integrated
the two solvers of CPLEX, CP and MIP, during the localization process. Specifically, during the
collection of constraints, we employ a variable to store information on the type of CSP being
constructed. When LocFaults identifies an erroneous path5 and before calculating MCSs, it
selects the appropriate solver based on the type of CSP associated with that path. If the CSP is
non-linear, it uses the CP OPTIMIZER solver; otherwise, it uses the MIP solver.
   For each benchmark, we provided an excerpt from the table containing the computation time6 .
Columns P and L represent the time of pretreatment and calculation of MCSs, respectively.


5
    An erroneous path is one on which we identify MCSs.
6
    The complete tables can be found at http://www.capv.toile-libre.org/Benchs_Mohammed.html#ravb, and the sources
    of these results are available at http://www.capv.toile-libre.org/Benchs_Mohammed.html#sr.
5.1.1. BubbleSort benchmark
BubbleSort is an implementation of the bubble sort algorithm. The erroneous statement in the
program causes the program to sort the input array by considering only its 𝑛 − 1 first elements,
leading to incorrect results. The malfunction of BubbleSort is due to the insufficient number of
iterations performed by the loop, which is caused by the faulty initialization of the variable 𝑖 as
𝑖 = 𝑡𝑎𝑏.𝑙𝑒𝑛𝑔𝑡ℎ − 1; the correct instruction should be 𝑖 = 𝑡𝑎𝑏.𝑙𝑒𝑛𝑔𝑡ℎ.
   The graph in Figure 4 depicts the variation in computation times for different versions of
LocFaults and BugAssist, based on the number of unfoldings.

                                                          LocFaults (= 0)
                                                          LocFaults (≤ 1)
                                          6,000           LocFaults (≤ 2)
                                                          LocFaults (≤ 3)
                     Times (in seconds)




                                                            BugAssist

                                          4,000



                                          2,000



                                             0
                                            10    5       15           20
                                              Unfoldings (𝑏)
Figure 4: Comparison of the time evolution of different versions of LocFaults and BugAssist for the
BubbleSort benchmark, with an increasing unwinding loop limit.


   The runtime of LocFaults and BugAssist shows exponential growth with the number of
unfoldings, with BugAssist consistently having the highest computation times. BugAssist may
not be effective for this benchmark. Among the different versions of LocFaults (with up to 3, 2,
1, or 0 conditions deviated), all remain usable up to a certain unfolding threshold. The number
of unfoldings at which the computation time of BugAssist becomes prohibitively high is lower
compared to LocFaults. Additionally, the computation time of LocFaults with up to 3 conditions
deviated is lower than that of LocFaults with up to 2 conditions deviated, which is also lower
than that of LocFaults with up to 1 condition deviated. The computation times of LocFaults
with up to 1 and 0 conditions deviated are nearly identical.

5.1.2. SquareRoot and Sum benchmarks
The SquareRoot program (refer to Figure 5) is designed to find the integer part of the square
root of the integer 50. An error is injected at line 13, resulting in the incorrect return value of
8, whereas the correct value should be 7. This program has been previously used in the paper
describing the BugAssist approach. It contains a linear numerical calculation in its loop and
non-linear calculation in its postcondition.
1    public class SquareRoot {
2        /*@ ensures((res*res<=val) && (res+1)*(res+1)>val);*/
3        public static int squareRoot ()
4        {
5            int val = 50;
6            int i = 1;
7            int v = 0;
8            int res;
9            while (v < val){
10               v = v + 2*i + 1;
11               i = i + 1;
12           }
13           res = i; //error: should be res = i-1
14           return res;
15       }
16   }

Figure 5: The SquareRoot program.


   With an unwinding limit of 50, BugAssist identifies the following suspicious instructions
for this program: {9, 10, 11, 13}. The localization time is 36.16𝑠 and the pre-treatment time is
0.12𝑠.
   LocFaults identifies suspicious instructions by providing their location in the program (in-
struction line), as well as the line of the condition and the iteration number of the loop leading
to that instruction. For example, {9 : 2.11} indicates that the suspicious instruction is on line
11 of the program, which is inside a loop with the stop condition at line 9 and the iteration
number is 2. The sets of suspected instructions identified by LocFaults are listed in Table 3. The

Table 3
MCD and MCSs calculated by LocFaults for SquareRoot.
                                    {5}, {6}, {9 : 1.11}, {9 : 2.11}, {9 : 3.11},
                      ∅
                               {9 : 4.11}, {9 : 5.11}, {9 : 6.11}, {9 : 7.11}, {13}
                                 {5}, {6}, {7}, {9 : 1.10}, {9 : 2.10}, {9 : 3.10},
                   {9 : 7}         {9 : 4.10}, {9 : 5.10}, {9 : 6.10}, {9 : 1.11},
                             {9 : 2.11}, {9 : 3.11}, {9 : 4.11}, {9 : 5.11}, {9 : 6.11}

pretreatment time is 0.769s. The time for exploring the CFG and calculating MCSs is 1.299s.
   We conducted a study of the times for LocFaults and BugAssist with values of "val" ranging
from 10 to 100 (where the number of unfoldings "b" used is equal to "val"), in order to analyze
the combinatorial behavior of each tool for this program.
∑︀The
   𝑛
         Sum program receives a positive integer 𝑛 from the user and calculates the value of
   𝑖=1 as per the∑︀
       𝑖            postcondition. The
                                     ∑︀error in Sum lies in the condition of its loop, causing it to
                      𝑛−1               𝑛
calculate the sum 𝑖=1 𝑖 instead of 𝑖=1 𝑖. The program contains linear numerical instructions
within the core of the loop, along with a nonlinear postcondition.
   The time results for the SquareRoot and Sum benchmarks are presented in Tables 4 and 5,
respectively. It is observed that the execution time of BugAssist increases rapidly, while the
times of LocFaults remain relatively constant. Furthermore, the times of LocFaults with at most
0, 1, and 2 conditions deviated are comparable to those of LocFaults with at most 3 conditions
deviated.
Table 4
Computation time for SquareRoot Benchmark.
                                               LocFaults                      BugAssist
         Program        b                              L
                                  P                                          P         L
                                         =0      ≤1      ≤2         ≤3
            V0      10        1.096𝑠    1.737𝑠 2.098𝑠 2.113𝑠      2.066𝑠    0.05𝑠     3.51𝑠
            V10     20        0.724𝑠    0.974𝑠 1.131𝑠 1.117𝑠      1.099𝑠    0.05𝑠     6.54𝑠
            V20     30        0.771𝑠    1.048𝑠 1.16𝑠 1.171𝑠       1.223𝑠    0.08𝑠    12.32𝑠
            V30     40        0.765𝑠    1.048𝑠 1.248𝑠 1.266𝑠       1.28𝑠    0.09𝑠    23.35𝑠
            V40     50        0.769𝑠    1.089𝑠 1.271𝑠 1.291𝑠      1.299𝑠    0.12𝑠    36.16𝑠
            V50     60        0.741𝑠    1.041𝑠 1.251𝑠 1.265𝑠      1.281𝑠    0.14𝑠    38.22𝑠
            V70     80        0.769𝑠    1.114𝑠 1.407𝑠 1.424𝑠      1.386𝑠    0.19𝑠    57.09𝑠
            V80     90        0.744𝑠    1.085𝑠 1.454𝑠 1.393𝑠      1.505𝑠    0.22𝑠    64.94𝑠
            V90     100       0.791𝑠    1.168𝑠 1.605𝑠 1.616𝑠      1.613𝑠    0.24𝑠    80.81𝑠

Table 5
Computation time for Sum Benchmark.
                                               LocFaults                         BugAssist
       Program     b                                   L
                              P                                               P         L
                                       =0        ≤1        ≤2        ≤3
          V0       6        0.765𝑠    0.427𝑠   0.766𝑠    0.547𝑠    0.608𝑠   0.04𝑠     2.19𝑠
          V10      16        0.9𝑠     0.785𝑠   1.731𝑠    1.845𝑠    1.615𝑠   0.08𝑠     17.88𝑠
          V20      26        1.11𝑠    1.449𝑠    7.27𝑠    7.264𝑠     6.34𝑠   0.12𝑠     53.85𝑠
          V30      36       1.255𝑠    0.389𝑠   8.727𝑠     4.89𝑠    4.103𝑠   0.13𝑠    108.31𝑠
          V40      46       1.052𝑠    0.129𝑠   5.258𝑠    5.746𝑠   13.558𝑠   0.23𝑠    206.77𝑠
          V50      56        1.06𝑠    0.163𝑠   7.328𝑠    6.891𝑠    6.781𝑠   0.22𝑠    341.41𝑠
          V60      66       1.588𝑠    0.235𝑠   13.998𝑠 13.343𝑠    14.698𝑠   0.36𝑠    593.82𝑠
          V70      76        0.82𝑠    0.141𝑠   10.066𝑠 9.453𝑠     10.531𝑠   0.24𝑠    455.76𝑠
          V80      86       0.789𝑠    0.141𝑠   13.03𝑠 12.643𝑠     12.843𝑠   0.24𝑠    548.83𝑠
          V90      96       0.803𝑠    0.157𝑠   34.994𝑠 28.939𝑠    18.141𝑠   0.31𝑠    785.64𝑠


6. Conclusion
The LocFaults method detects suspicious subsets by analyzing the paths of the CFG to identify
the MCDs and MCSs from each MCD, utilizing constraint solvers. On the other hand, the
BugAssist method calculates the merger of MCSs by transforming the entire program into a
Boolean formula and leveraging Max-SAT solvers. Both methods start from a counterexample to
identify potential issues. In this paper, we have presented a scalability exploration of LocFaults,
with a focus on handling loops with the Off-by-one bug. The initial results indicate that LocFaults
is more effective than BugAssist for programs with loops. The execution times of BugAssist
tend to rapidly increase with the number of loop unfoldings, while LocFaults shows better
scalability in this aspect.
   As part of our future work, we plan to validate our results on programs with more complex
loops. We also intend to compare the performance of LocFaults with existing statistical methods.
To further enhance our tool, we are developing an interactive version that presents suspect
subsets one by one, leveraging the user’s knowledge to select the conditions that should be
deviated. Additionally, we are considering ways to extend our method to handle numerical
instructions involving calculations on floating-point


References
 [1] R. N. Charette, Why software fails, IEEE spectrum 42 (2005) 36.
 [2] M. Bekkouche, Bug stories, 2015. URL: http://www.capv.toile-libre.org/Bug_stories.html.
 [3] W. E. Wong, R. Gao, Y. Li, R. Abreu, F. Wotawa, A survey on software fault localization,
     IEEE Transactions on Software Engineering 42 (2016) 707–740.
 [4] M. Bekkouche, H. Collavizza, M. Rueher, Locfaults: A new flow-driven and constraint-
     based error localization approach, in: Proceedings of the 30th Annual ACM Symposium
     on Applied Computing, 2015, pp. 1773–1780.
 [5] V. D’silva, D. Kroening, G. Weissenbacher, A survey of automated techniques for formal
     software verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits
     and Systems 27 (2008) 1165–1178.
 [6] J. A. Jones, M. J. Harrold, J. Stasko, Visualization of test information to assist fault
     localization, in: Proceedings of the 24th international conference on Software engineering,
     2002, pp. 467–477.
 [7] J. A. Jones, M. J. Harrold, Empirical evaluation of the tarantula automatic fault-localization
     technique, in: Proceedings of the 20th IEEE/ACM international Conference on Automated
     software engineering, 2005, pp. 273–282.
 [8] R. Abreu, P. Zoeteweij, A. J. Van Gemund, On the accuracy of spectrum-based fault
     localization, in: Testing: Academic and industrial conference practice and research
     techniques-MUTATION (TAICPART-MUTATION 2007), IEEE, 2007, pp. 89–98.
 [9] M. Y. Chen, E. Kiciman, E. Fratkin, A. Fox, E. Brewer, Pinpoint: Problem determination in
     large, dynamic internet services, in: Proceedings International Conference on Dependable
     Systems and Networks, IEEE, 2002, pp. 595–604.
[10] A. Zakari, S. P. Lee, I. A. T. Hashem, A single fault localization technique based on failed
     test input, Array 3 (2019) 100008.
[11] A. Dutta, K. Kunal, S. S. Srivastava, S. Shankar, R. Mall, Ftfl: A fisher’s test-based approach
     for fault localization, Innovations in Systems and Software Engineering 17 (2021) 381–405.
[12] A. Majd, M. Vahidi-Asl, A. Khalilian, B. Bagheri, Consilientsfl: using preferential voting
     system to generate combinatorial ranking metrics for spectrum-based fault localization,
     Applied Intelligence 52 (2022) 11068–11088.
[13] Q. I. Sarhan, Á. Beszédes, Poster: Improving spectrum based fault localization for python
     programs using weighted code elements, in: 2023 IEEE Conference on Software Testing,
     Verification and Validation (ICST), IEEE, 2023, pp. 478–481.
[14] M. Jose, R. Majumdar, Cause clue clauses: error localization using maximum satisfiability,
     ACM SIGPLAN Notices 46 (2011) 437–446.
[15] M. Jose, R. Majumdar, Bug-assist: Assisting fault localization in ansi-c programs, in:
     Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT,
     USA, July 14-20, 2011. Proceedings 23, Springer, 2011, pp. 504–509.
[16] M. Barnett, K. R. M. Leino, Weakest-precondition of unstructured programs, in: Proceed-
     ings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools
     and engineering, 2005, pp. 82–87.
[17] H. Collavizza, M. Rueher, P. Van Hentenryck, Cpbpv: a constraint-programming framework
     for bounded program verification, Constraints 15 (2010) 238–264.
[18] M. H. Liffiton, K. A. Sakallah, Algorithms for computing minimal unsatisfiable subsets of
     constraints, Journal of Automated Reasoning 40 (2008) 1.
[19] E. Clarke, D. Kroening, F. Lerda, A tool for checking ansi-c programs, in: Tools and
     Algorithms for the Construction and Analysis of Systems: 10th International Conference,
     TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of
     Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004. Proceedings 10, Springer,
     2004, pp. 168–176.
[20] J. Marques-Silva, The msuncore maxsat solver, SAT (2009) 151.

</pre>