# Towards Extending the Range of Bugs That Automated Program Repair Can
handle††thanks: This work has been financially supported by the Research
Council of Norway through the secureIT project (RCN contract #288787).

Omar I. Al-Bataineh  Simula Research Laboratory
Oslo, Norway
<EMAIL_ADDRESS>Leon Moonen  Simula Research Laboratory
Oslo, Norway
<EMAIL_ADDRESS>
###### Abstract

Modern _automated program repair_ (APR) is well-tuned to finding and repairing
bugs that introduce _observable_ erroneous behavior to a program. However, a
significant class of bugs does not lead to such observable behavior (e.g.,
liveness/termination bugs, non-functional bugs, and information flow bugs).
Such bugs can generally not be handled with current APR approaches, so, as a
community, we need to develop complementary techniques.

To stimulate the systematic study of alternative APR approaches and hybrid APR
combinations, we devise a novel bug classification system that enables
methodical analysis of their bug detection power and bug repair capabilities.
To demonstrate the benefits, we analyze the repair of termination bugs in
sequential and concurrent programs. The study shows that integrating dynamic
APR with formal analysis techniques, such as termination provers and software
model checkers, reduces complexity and improves the overall reliability of
these repairs.

###### Index Terms:

automated program repair, bug classification, non-observable and liveness
bugs, hybrid techniques.

##  I Introduction

Corrective maintenance, i.e., finding and repairing software defects, is one
of the main categories of software maintenance, and responsible for a large
part of the overall costs of software development [1]. _Automated program
repair_ (APR) promises to increase developer productivity and drastically
reduce the costs of corrective maintenance [2, 3]. Despite the advances of APR
for real-world programs [4], these approaches can only handle certain types of
bugs because they generally rely on dynamic analysis for functional
verification, where a test suite is used to simulate the input and monitor the
output to check correct behavior. However, this is only viable if the effects
of a bug can be observed when executing the program.

Detecting and repairing _non-observable bugs_ and _liveness bugs_ (i.e., bugs
that do not lead to incorrect results or crashes) pose a far greater
challenge. For example, identifying a liveness bug requires finding an
infinite execution that will never satisfy the desired liveness property [5].
It is not known how long one would need to run the program to reveal an
existing liveness bug, making it impractical to find such cases using dynamic
analysis. Another critical challenge that makes detection and repair of
liveness bugs notoriously hard is that the effects that a liveness bug is
triggered are generally unobservable (i.e., they typically produce little
debugging information). One option for finding this class of bugs is applying
formal program analysis techniques that use correctness specifications to
detect liveness bugs. Such a rigorous analysis can both help to detect the
presence of liveness bugs as well as assure the absence of these bugs in
automatically generated patches.

The question which (combinations of) techniques will be most effective at
handling certain bugs is an open research question that forms the foundation
of this paper. To stimulate the systematic study of alternative APR approaches
and hybrid APR combinations, we devise a novel bug classification system that
enables methodical analysis of their bug detection power and bug repair
capabilities. In earlier work, various bug classification schemes were
developed to understand when and why specific bugs arise, and how they are
fixed. These classifications use a number of criteria, such as cause-impact
[6, 7], severity-priority [8], and bug complexity [9]. However, since they
were designed for different goals, they do not capture the properties required
to determine if a bug is amenable to a particular technique. To that end, we
introduce a bug classification system explicitly aimed at comparing different
techniques and evaluating the feasibility of their integration.

Contributions: (1) We propose a _novel bug classification system_ based on
three fundamental properties: _bug observability_ , _bug reproducibility_ ,
and _bug tractability_. This classification provides the APR community with a
tool to methodologically explore and compare alternative and hybrid APR
approaches by (i) analyzing the detection power of different bug detection
techniques, (ii) distinguishing APR approaches based on their bug repair
capabilities, and (iii) providing a common terminology that helps identify
gaps in current APR research.

(2) We discuss four _APR approaches_ that can handle different classes of
bugs: _dynamic APR_ , _static APR_ , _dynamic-static APR_ , and _formal APR_.
Moreover, we identify the conditions under which each approach can be
effectively applied.

(3) To demonstrate the benefits of our method, we study _termination bugs_ in
sequential and concurrent programs, and sketch novel _hybrid APR algorithms_
for repairing such bugs. The study shows that termination bugs in _sequential_
programs can be effectively addressed using _dynamic-static APR_ , by first
generating plausible patches using test cases and then using termination
provers [10, 11, 12] to check their correctness. The non-deterministic nature
of termination bugs in _concurrent_ programs makes them challenging for
dynamic analysis, and they are best addressed with _formal APR_ that combines
termination provers with software model checkers [13, 14, 15, 16, 17, 18, 19].

##  II Bug Classification Schemes

There are many different ways to expose bugs in programs, including manual
inspection, dynamic analysis (testing), static analysis, model checking, or a
combination of these techniques. Effective bug classification schemes can help
understand why bugs arise and how to fix them. Classification can also help
identify the most appropriate analysis technique for handling each class of
bugs. Next, we discuss three existing bug classification systems, analyze
their limitations, and introduce a new classification system that addresses
them:

  1. 1.

_Cause-impact criteria_ [6, 7]: Bugs are classified based on their cause:
algorithmic, concurrency, memory, generic programming, and unknown, as well as
based on their impact: security, performance, failure, and unknown.

  2. 2.

_Severity and priority criteria_ : This classification is used in many bug
tracking systems [8]. Severity indicates the impact of the bug on the
program’s functionality and can be categorized as critical, major, moderate,
minor, etc. Priority indicates how soon the bug should be fixed and is
categorized into levels such as low, medium, and high.

  3. 3.

_Bug complexity criteria_ [9]: These criteria distinguish four main
categories: (i) easy to detect, easy to repair bugs, (ii) easy to detect,
difficult to repair bugs, (iii) difficult to detect, easy to repair bugs, and
(iv) difficult to detect, difficult to repair bugs.

These three existing bug classification systems were not designed for
comparing the capabilities and limitations of different bug detection or
program repair techniques. As a result, their criteria do not capture the
specific properties needed to determine whether a bug $b$ is amenable to a
particular technique $T$. To address this gap, we propose a new bug
classification system that is based on three key properties of bugs, namely
_bug observability_ , _bug reproduciblity_ , and _bug tractability_. In
Sections III and IV, these properties are then used to analyze the power of
different bug detection techniques and APR approaches.

Before proceeding further, let us first define a program bug. We base
ourselves on a specification of _expected behavior_ : the expected responses
(output) of the program to a given input.

######  Definition 1 (Program bug)

Let $P$ be a program, $I$ a set of inputs, and $\varphi_{beh}$ be a
specification of expected behavior of $P$. We say that $P$ suffers from a bug
iff there exists at least one input $i\in I$ that leads to an execution trace
under which program $P$ violates $\varphi_{beh}$, formalised as
$(P,i)\not\models\varphi_{beh}$.

Since a complete specification of a program’s expected behavior is often not
available, test cases are generally used to model the expected behavior of a
program $P$. We assume there exists $(i,o_{exp})$, where $o_{exp}$ is the
expected output for input $i\in I$. When the observed output $o_{obs}=(P,i)$
does not match the expected output $o_{exp}$, we say that $P$ contains a bug.

######  Definition 2 (Observable bug)

Let $P$ be a program containing bug $b$. We say that $b$ is an _observable
bug_ iff there exists an execution of $P$ where, in a finite number of
execution steps, the erroneous behavior of $b$ can be seen by an observer $O$.

######  Definition 3 (Classifying bugs by observability)

We classify bugs based on the notion of observability in three types:

  1. 1.

_observable bugs_ whose erroneous behavior is fully observable in finite
execution steps (e.g., arithmetic bugs),

  2. 2.

_partially observable bugs_ whose erroneous behavior is only partially
observable at runtime because the faulty trace is infinite, so not all output
of the program can be observed (e.g., termination bugs),

  3. 3.

_non-observable bugs_ whose erroneous behavior is fully unobservable at
runtime (e.g., non-functional bugs).

Note that observability is a relative notion that depends on the observation
power of $O$. In the simplest case, the observer can witness the output
produced by $P$ and the corresponding execution time. If we increase the
observation power of $O$ (i.e., the amount of information $O$ can gather about
the program’s execution), some non-observable bugs may become observable. For
example, bugs that adversely affect the memory or energy consumption can
easily go unnoticed during the execution of the program. Such bugs can be
exposed by using monitoring at the virtual machine or operating system level
[20, 21, 22, 23]. Alternatively, the program can be augmented with additional
variables and checks that help to keep track of these non-functional aspects
at runtime [24]. However, increasing observation power also increases the
chance of affecting the program’s execution [25].

We distinguish five common types of observable erroneous behavior:
$EB=\\{$crash, exception, incorrectResult, softHang, hardHang$\\}$. While most
types in $EB$ are easy to understand, we will define the notions of _soft_ and
_hard_ hang bugs. Hang bugs are a particular type of bugs that concern
(temporary or permanent) lack of progress in observable behavior [26, 27].
Hang bugs can have various causes, such as iteration errors or communication
deadlocks. To define hang bugs, we use a temporal specification [28, 29] that
checks if any of the locations where the program might terminate can be
reached.

######  Definition 4 (Halting Statements)

We refer to a statement $s$ in a program $P$ as a _halting statement_ iff the
expected behavior of $P$ is that execution terminates after executing
statement $s$.

Examples of halting statements include special termination statements such as
exit, or simply the final statement in a program. Observe that programs whose
expected behavior is to never terminate have no halting statements (e.g., a
webserver).

######  Definition 5 (Hang bugs)

Let $P$ be a program with a set of inputs $I$ and $H$ be the set of halting
statements of $P$. Let $\varphi_{temp}$ be a temporal property that puts an
upper bound on the execution time of $P$, and $\varphi_{reach}$ be a temporal
property that checks whether $P$ reaches a halting statement. Let also
$EB^{\prime}=EB~{}\backslash~{}\\{\text{\emph{softHang}},\text{\emph{hardHang}}\\}$.
We distinguish:

  1. 1.

Soft hang bugs occur when there exists an input $i\in I$ that makes $P$
unresponsive for a finite amount of time before execution is resumed and a
halting statement is reached:

$S:(P,i)\not\models\varphi_{temp}~{}\land(P,i)\models\varphi_{reach}\land~{}\text{\emph{output(P,
i)}}\not\subseteq EB^{\prime}\vspace{-1.3ex}$

  2. 2.

Hard hang bugs, also known as termination bugs, occur when there exists an
input $i\in I$ that makes $P$ unresponsive for an unbounded amount of time,
never resuming to normal execution or reaching a halting statement:

$H:(P,i)\not\models\varphi_{temp}~{}\land(P,i)\not\models\varphi_{reach}~{}\land~{}\text{\emph{output(P,
i)}}\not\subseteq EB^{\prime}\vspace{-.5ex}$

Hang bugs are also referred to as _liveness violations_ in model checking and
formal program analysis literature [30, 31, 32, 33], and we will use these
terms interchangeably in the remainder.

We now turn to discuss the property of bug reproducibility.

######  Definition 6 (Bug reproducibility)

Let $P$ be a program containing a bug $b$ and $t_{b}$ be a test case that
exposes $b$. We say that $b$ is a _reproducible_ or _deterministic bug_ iff
every time program $P$ is executed under test $t_{b}$, bug $b$ is exposed and
the same erroneous behavior is observed. On the other hand, we say that $b$ is
a _hard-to-reproduce_ or _non-deterministic bug_ iff bug $b$ is exposed in
rare circumstances when repeating the execution of $P$ under test $t_{b}$
(i.e., the result of program $P$ depends not only on the code of $P$ but also
on the timing of the execution).

TABLE I: A summary of the key properties for bug classification with their attributes and impact bug property | property attributes | impact on bug detection techniques
---|---|---
observability |  $\\{$observable, partially-observable, non-observable$\\}$ | affects detection power
reproducibility |  $\\{$easy-to-reproduce, hard-to-reproduce$\\}$ | affects efficiency and scalability
tractability |  $\\{$shallow, deep, liveness$\\}$ | affects detection power and efficiency

Reproducible bugs are easy to detect, provided that the bug is observable (see
Definition 2). Not surprisingly, hard-to-reproduce bugs are also hard to
detect. Arithmetic bugs are examples of _easy-to-reproduce_ bugs, while
concurrency bugs are examples of _hard-to-reproduce_ bugs. The last property
we study is _bug tractability_ , which depends on the _depth_ of the bug and
the size of the faulty trace it produces.

######  Definition 7 (Bug tractability)

Let $P$ be a program containing bug $b$ and $L$ be the set of reachable
locations of $P$ and $\ell_{b}\in L$ be the buggy location to the bug $b$. We
say that the trace of $b$ is a _tractable trace_ iff for each execution of $P$
that is buggy to $b$, the number of execution steps that are required to reach
$\ell_{b}$ is bounded and that $\ell_{b}$ is not part of a loop that can be
executed infinitely often. On the other hand, we say that the trace of $b$ is
_intractable_ iff $\ell_{b}$ is visited infinitely often during the execution
of $P$ (i.e., $\ell_{b}$ is part of an infinite loop).

The presence of loops plays a crucial role in determining the tractability of
a bug. The size of faulty traces for non-loop programs is typically shorter
than those in loop programs. Based on the size of the faulty trace, we can
further distinguish the class of tractable bugs: (i) _shallow bugs_ are
tractable bugs with finite short faulty traces, (ii) _deep bugs_ are tractable
bugs with finite but long faulty traces. For example, a bug in a loop program
$P$ that does not occur until a vast number of iterations are executed can be
viewed as an example of a deep bug.

Bug Classification System: Table I summarises the three properties in our
classification system with their distinguishing attributes and impact on bug
detection. Our classification system associates each bug with a three-tuple of
concrete attributes for _$\\{$ observability, reproducibility,
tractability$\\}$_. For example, an arithmetic bug has the properties: _$\\{$
observable, easy-to-reproduce, shallow$\\}$_.

##  III Bug Detection Techniques

Various bug detection techniques can be used to expose bugs in programs. In
this work, we are interested in studying three well-known bug detection
techniques: dynamic analysis, static analysis, and model checking. While
dynamic analysis detects bugs in programs by executing them, static analysis
and model checking use different techniques in bug detection that perform bug
checking statically, without running the program. We start by discussing the
requirements needed to expose bugs in each technique, the advantages and
disadvantages of the techniques, and the theoretical foundation and detection
power of each (i.e., the classes of bugs that each technique can handle).

###  III-A Dynamic Analysis

Dynamic analysis is a technique to identify bugs and vulnerabilities in
programs by exercising various runs through the program based on valid inputs.
Dynamic analysis can be performed using a test suite, which can be developed
manually or via test case generation, or through fuzzing, which systematically
explores a large amount of automatically generated tests. Fuzzing is one of
the most common methods used to find vulnerabilities in programs [34, 35].
Early fuzz testing was based on sending random inputs to a program to check if
it could be made to crash. The techniques have evolved to systematically
explore the input space using knowledge from the source code or input formats
to discover bugs that are hidden deep in the code.

Dynamic analysis has several advantages over the other program analysis
techniques: (i) the program behavior can be monitored, and bugs can be exposed
while the program is running; (ii) it allows for analysis of programs for
which we do not have access to the actual code; (iii) it can be conducted
against any program; and last but not least, (iv) it can identify bugs that
are hard to find using static analysis. We now discuss the conditions under
which bugs may be discovered in dynamic analysis.

######  Definition 8 (Bug detection in dynamic analysis)

Let $P$ be a program containing bug $b$, and $D$ be a dynamic program analysis
checker (i.e., an automated testing tool such as a fuzzer). We say that $b$ is
detectable in $D$ iff

  1. 1.

$P$ is given in an executable form,

  2. 2.

bug $b$ is _observable_ in some executions of $P$,

  3. 3.

there exists a test suite $T$ containing at least one failing test $t$ by
which bug $b$ can be exposed in $P$.

However, many bugs whose detection requires the analysis of infinite traces or
the satisfaction of complex composite properties cannot be found using an
approach solely relying on test cases. Examples of such classes of bugs
include (i) bugs in non-executable programs, (ii) liveness bugs such as
termination and starvation bugs, and (iii) non-observable bugs such as non-
functional and information flow bugs [36, 37].

###### Observation 1

Dynamic analysis techniques can handle observable classes of bugs with finite
execution traces, provided that a testing mechanism is implemented by which
the bug can be exposed, and provided that the program is executable.

To address these limitations, we need to pair dynamic analysis with
complementary bug detection techniques to improve the detection power of the
approach. The remainder of this section discusses static analysis and model
checking, which instead of using the program itself as in dynamic analysis,
analyzes abstractions of the program, to improve observability and
tractability and enable the detection of deeper bugs [38].

###  III-B Static Program Analysis

Static program analysis is an approach for analyzing a computer program
without actually executing it. The most significant advantage of static
analysis is the ability to quickly and automatically examine the complete code
of the program to find flaws that might be missed by dynamic analysis. The
literature on static program analysis for bug detection is rich and mature
[39, 40, 41]. Many of these techniques build on automatically evaluated
analysis rules and bug detection patterns that capture the general conditions
under which specific bugs can occur, providing a systematic way for their
detection.

To capture the notion of bug detectability in static analysis, one needs to
ensure the availability of the source code of the buggy program at which the
bug $b$ occurs and the availability of some valid solid theory for the
detection of bug $b$.

######  Definition 9 (Bug detection in static analysis)

Let $P$ be a program containing bug $b$ and $S$ be a static program analyzer
that can be used to expose bugs of type $b$. We say that $b$ is a bug
detectable by analyzer $S$ if all of the following conditions hold:

  1. 1.

the source code of $P$ is available, and

  2. 2.

$S$ contains sound and complete detection method for $b$, and

  3. 3.

$P$ is written in a language that is accepted by $S$.

The increasing complexity of (loop) programs and the large variety of
vulnerabilities make it difficult for static code analyzers to detect and
identify vulnerabilities in a precise manner. One of the most significant
disadvantages of the static code analysis methodology is the presence of
false-positive warnings: the tool may signal possible bugs where there are
none. However, reducing the number of false positives in static analysis tools
is still an open problem.

###### Observation 2

Static checkers can handle observable, non-observable, reproducible, and non-
reproducible bugs, provided that the checker is built based on some solid
mathematical foundation, and provided that the source code of the program is
available in a programming language accepted by the checker.

Dynamic and static analysis techniques have different bug detection powers as
they rely on distinct assumptions and use orthogonal detection methods.
Overall, these techniques have complementary strengths and weaknesses that are
worth combining to improve the reliability of APR systems.

###  III-C Model Checking

Model checking [42, 43, 44] is an automated formal method for checking whether
a finite-state model of a system meets a given specification. The technique
has been used successfully to debug complex computer hardware, concurrent
systems, and real-world safety-critical systems.

Model checking has several advantages. It can detect errors that would be very
difficult to notice with other methods, such as in concurrent programs. The
properties that can be verified are more expressive than with traditional
testing, depending on the formalism used to express them. For example,
properties that require something to happen infinitely often, or properties
that require that some alternative is always available. In addition, because
every possible behavior of the model is checked, the result is inevitable,
provided that the model checking tool itself has no serious errors.

Model checking can be an expensive procedure in a repair process because of
its exhaustive nature. Expressing both the model of the system and the
properties formally requires great care and expertise. Moreover, one of the
most significant problems with model checking in practice is the so-called
“state explosion problem”: When the number of state variables in the system
increases, the size of the system state space grows exponentially. However,
abstractions can be applied to bring the verification within feasible bounds
of model checking technology.

Software model checking tools [13, 14, 15, 16, 17, 18, 19] verify the
correctness of software models in a rigorous and automated fashion. Most tools
construct a (symbolic) reachability graph for the program-under-analysis
(i.e., a graph that contains reachable run-time states of the program)
_without_ running the program. This graph is then used to check if a property
of interest holds. They typically implement sophisticated data structures that
enable clever search algorithms and optimizations.

The answer returned by a model checker is either a notion of a successful
verification (i.e., the specification holds), or a counterexample – an
execution path that violates a given property. However, if the program being
verified has an infinite state space, certain types of abstractions are
needed, or the analysis may simply not terminate.

######  Definition 10 (Bug detection in model checking)

Let $P$ be a program containing bug $b$ and SMC be a software model checker
that can be used to expose bugs of type $b$. We say that $b$ is a detectable
bug in the model checker SMC iff:

  1. 1.

a formal property $\varphi_{\text{\emph{b}}}$ is available that is written in
the input specification language of SMC, which captures the conditions under
which $b$ can occur, and

  2. 2.

the source code of $p$ is available, and

  3. 3.

$P$ has finite states or an equivalent finite abstract program $P_{abs}$ can
be constructed for the properties of interest, and

  4. 4.

the program $P$ or its reduced equivalent program $P_{abs}$ is written in a
modeling language that is acceptable by SMC.

TABLE II: A summary of key differences and similarities of dynamic analysis,
static analysis, and model checking

criteria | dynamic analysis | static analysis | model checking
---|---|---|---
bug detection mechanism | test cases | pattern-based specifications | formal correctness specifications
accuracy of the analysis | accurate | inaccurate (suffers from false positives) | accurate relative to the accuracy of model
the need of code availability | not needed | needed to perform the analysis | needed to construct the model
the need of bug observability | needed to detect the bug | not needed (performs code analysis) | not needed (performs state analysis)
code coverage of the program | incomplete code coverage | complete code coverage | complete code coverage
the need of code executability | needed to detect the bug | the program will not be executed | the program will not be executed
language dependency | language-independent | language dependent | language dependent
automation of the analysis | can be automated (fuzz testing) | fully automated | a model needs to be manually written

###### Observation 3

Model checking tools can handle observable, non-observable, reproducible, and
non-reproducible bugs, provided that the size of the program is finite or a
sound abstraction can be developed to bring the program within the feasibility
bound of model checking, and provided that a specification is available for
the bug of interest.

Bug Detection Properties: Based on the characteristics of the three bug
detection techniques discussed, one can make the following general
observations. Model checking is more expensive than static analysis, requiring
longer running times and more resources. Static analysis is not as accurate as
model checking, and testing is not as complete as model checking. Testing
suffers from coverage challenges: it is challenging to cover all possible
executions of the program, in particular for programs with an infinite input
space where this becomes prohibitively expensive. To ensure the correctness of
the program for all inputs, a correctness specification must exist that can be
formally analyzed.

Table II summarises the key differences and similarities between the three
program analysis techniques using several criteria: code coverage, the need
for code executability, accuracy of the analysis, the need for bug
observability, the need for code availability, and automation of the
technique. By code coverage, we mean the number of feasible execution paths of
the program that the technique can cover during the analysis, and accuracy
indicates whether the detected bug is a real bug.

##  IV APR Approaches

This section describes four APR approaches that can handle different classes
of bugs. The four approaches combine the detection power of dynamic analysis,
static analysis, and model checking techniques to improve the reliability of
existing APR techniques. We discuss the applicability of these approaches to
three classes of bugs: arithmetic bugs (observable bugs), non-functional bugs
(non-observable bugs), and liveness bugs (partially observable bugs).

An APR approach generally consists of four steps: fault identification, fault
localization, patch generation, and patch validation. The most challenging
step in the APR process is the patch validation step, in which the generated
patch is extensively evaluated to ensure that the bug is resolved, and that
the patch does not introduce any unwanted behavior. In dynamic APR, as the
name implies, the patch validation step is primarily performed using test
cases. Since these rarely capture the expected behavior in full detail, the
technique suffers from the so-called patch overfitting problem, where the
patched program may pass the tests in the given test suite, while it is
failing for valid inputs not covered by the test suite. It is therefore
desirable to combine the power of different analysis techniques while taking
into account the distinctive properties of each class of bugs. This leads to
our examination of the following four APR approaches:

  1. 1.

_dynamic APR_ : in which fault identification and patch validation are
performed using dynamic analysis techniques. GenProg [45] is an example of a
dynamic APR tool;

  2. 2.

_static APR_ : in which fault identification and patch validation are
performed using static analysis techniques;

  3. 3.

_dynamic-static APR_ : in which fault identification and patch validation are
performed using a combination of static and dynamic analysis, i.e., using test
cases and static analysis tools developed for the same class of bugs;

  4. 4.

_formal APR_ : in which fault identification and patch validation are
performed using formal methods and verification techniques such as model
checking.

A hybrid APR approach aims to improve the overall quality of the generated
repairs and alleviate the patch overfitting challenge of dynamic APR systems.

###  IV-A Arithmetic Bugs

Arithmetic calculations affect a wide variety of applications, including
safety-critical systems such as control systems for vehicles, medical
equipment, and industrial plants. The key properties of arithmetic bugs can be
summarised as follows:

  1. 1.

Arithmetic bugs are observable classes of bugs or can be easily made
observable to external observers: the root causes of arithmetic bugs are
limited and easy to identify.

  2. 2.

Arithmetic bugs are tractable bugs with finite traces.

  3. 3.

Arithmetic bugs introduce various erroneous behavior to the program in which
they occur: they may cause the program to crash or may produce incorrect
outputs.

These properties make them directly amenable to dynamic (i.e., test-based)
APR. Note that many of the available dynamic APR systems rely explicitly or
implicitly on observability strategies to expose this class of bugs (e.g.,
integer overflow, division by zero, etc.). There are also several static
analysis tools that can handle arithmetic bugs. Thus, arithmetic bugs can be
repaired using dynamic APR, static APR, or dynamic-static APR. These repair
approaches differ mainly in the correctness specification used to validate
generated patches for the detected arithmetic bug. In dynamic APR, the
specification is captured by the test cases, while in static APR, the
specification is captured by the formal bug detection rules.

###### Example 1

Integer overflow (IO) is a type of arithmetic bug that occurs when the
computation of an arithmetic operation, such as multiplication or addition,
exceeds the maximum size of the integer type used to store it. IO bugs are an
observable class of bugs, and thus they are amenable to dynamic APR. IO bugs
are also amenable to static APR, and there are several reliable static
analysis tools available that can address IO bugs [46, 47]. Thus, devising a
hybrid static-dynamic APR system for IO bugs is feasible and will help
increase confidence about the soundness of the generated repairs.

###### Observation 4

Arithmetic bugs are observable, tractable, and reproducible classes of bugs
with finite execution traces. They are amenable to both dynamic and static APR
since the root causes of arithmetic bugs are easy to identify.

###  IV-B Non-functional Bugs

Non-functional bugs [48, 49, 24] are a class of bugs that affect the way a
program operates, rather than the functional behavior of the program.
Inefficiently written loops in programs and synchronization issues in
concurrent programs (i.e., using a large unnecessary number of locks) can be
viewed as examples of non-functional bugs. Non-functional bugs are as
important as functional bugs. For example, energy consumption saving is
getting more urgent, particularly for applications running on embedded systems
and IoT in Smart Cities.

Fixing non-functional bugs is generally more complex than fixing functional
bugs, since non-functional bugs can hide themselves well in the code. While
most functional bugs can be detected through observing the erroneous behavior
of bugs, a large percentage of non-functional bugs are detected through manual
code review [50, 51, 52]. Non-functional bugs usually do not generate
incorrect results or crashes. Therefore, they cannot be observed by checking
the program output. The key properties of non-functional bugs can be described
as follows.

  1. 1.

Non-functional bugs are generally non-observable classes of bugs: they do not
introduce direct observable erroneous behavior to the program in which they
occur.

  2. 2.

Non-functional bugs increase the anticipated running cost of a program
(execution time, memory and energy consumption, etc.) due to the inefficient
use of resources.

Depending on what quality attributes are considered, programs may suffer from
many different types of non-functional bugs. For example, consider the class
of non-functional bugs that adversely affect the run-time costs of executing
the program, such as execution time, memory consumption, and energy
consumption. To expose such types of bugs, the program may need to be
augmented with additional variables or online monitors that can be used to
observe aspects at runtime [24].

Therefore, there is a need to develop effective bug detection tools that can
be used to expose non-functional bugs at the early stages of the software
development life cycle. Specifically, this requires efficient profiling
techniques and oracles that help decide whether the program’s non-functional
requirements are met under a particular workload. Unfortunately, the lack of
effective test oracles for non-functional bugs is a well-known problem that
will need to be addressed in the future.

###### Observation 5

Non-functional bugs are an example of non-observable classes of bugs (i.e., a
program that suffers from a non-functional bug executes normally and
terminates normally). Thus, they are not directly amenable to traditional
dynamic bug detection techniques that rely on test cases and observing a
program’s outputs.

###  IV-C Liveness Bugs

In this section, we discuss a class of bugs that has received little attention
from the APR community, namely liveness bugs. A _liveness property_ asserts
that “something good will eventually occur when executing a program” [30, 31].
Freedom of starvation and program termination are examples of liveness
properties. A program that violates a liveness property cannot make progress
and thus suffers from a _liveness bug_.

Two fundamental properties make detecting and repairing liveness bugs far more
challenging than other classes of bugs. First, the behavioral effects of
triggering a liveness bug are generally unobservable. Second, identifying a
liveness bug requires finding an infinite execution that will never satisfy
the desired liveness property [5], making it impractical to find such bugs
using dynamic analysis. Therefore, detecting and repairing liveness bugs
generally require more sophisticated repair algorithms since they must be able
to generate a finite representation of infinite counterexamples.

To better understand the complexity of repairing liveness bugs, we study a
subset of liveness bugs known as termination bugs. There are two advantages to
this choice: On the one hand, a termination bug is a specific type of liveness
bug whose repair is essential for ensuring software reliability. On the other
hand, by examining techniques for handling termination bugs, we gain knowledge
that can help address other liveness bugs. Termination bugs have the following
specific properties:

  1. 1.

Termination bugs are _partially observable_ : an observer monitoring the
behavior of a non-terminating loop program will not witness any erroneous
behavior but rather experience unexpectedly long execution times. The only
observable behavior of termination bugs is that the program becomes _non-
responsive at runtime_.

  2. 2.

Termination bugs have _infinite faulty traces_ : a counterexample to a
termination property violation is infinite.

###### Observation 6

Termination bugs are an example of partially observable bugs with infinite
execution traces. Termination bugs are amenable to dynamic-static APR and
static APR.

##  V Hybrid APR for Termination Bugs

This section describes a hybrid program repair approach for termination bugs
that combines the strengths of termination provers with those of software
model checkers. Such a combination has two key advantages. First, it
considerably reduces the overall computational complexity of the problem by
avoiding the exhaustive exploration of the program’s input space. Second, it
helps avoid the known overfitting problem by generating verified repairs for
termination bugs.

The presence of loops in programs can complicate the detection of certain
classes of bugs. Recall the two types of hang bugs from Definition 5; It is
not clear how one can distinguish between the following two types of loops
using a dynamic analysis technique: (i) inefficiently written loops that
introduce a soft hang bug, and (ii) incorrect infinite loops that introduce a
hard hang or termination bug.

Earlier work [53] that evaluated the effectiveness of different APR tools on
the ManyBugs and IntroClass datasets, used a simple timeout mechanism to
handle termination bugs in these two datasets: when the execution time of a
program exceeds some pre-specified period, they consider the program to be
_likely_ non-terminating due to an infinite loop. Marcote and Monperrus
instrument loops with iteration counters that are monitored to detect infinite
loops [54]. Both options _can_ lead to false conclusions about the program
under analysis (i.e., even when the watchdog triggers, the program may not
have a termination bug but suffer from a soft hang bug). Moreover, hang bugs
can have complicated causes: programs that become unresponsive may contain
deadlocks, infinite loops, or other bugs that lead to non-termination but are
_not_ infinite loops.

An effective solution for addressing termination bugs is to apply _termination
provers_ : tools that can check combinations of many complex termination
criteria. They take a program as input and return one of three answers:
_terminating_ (TR), _non-terminating_ (NT), or _unknown_ (UN). In general,
when the prover returns definite answer for a given program (i.e.,
$\text{\emph{answer}}\in\\{\text{\emph{TR}},\text{\emph{NT}}$}), the answer is
valid with high confidence. Termination provers have been successfully used to
analyse termination of a wide variety of loop programs [55, 58, 59, 60, 61,
62, 63, 64, 65, 56, 57].

######  Definition 11 (Valid Termination Bug Repair)

Let $P$ be a buggy non-terminating program with a set of inputs $I$,
$\varphi_{beh}$ a specification of expected behavior of $P$, and
$\varphi_{reach}$ a specification that checks the reachability of some halting
statement of $P$. We say that $P^{\prime}$ is a valid repair of $P$ iff for
every input $i\in I$ we have $(P^{\prime},i)\models\varphi_{beh}$ and
$(P^{\prime},i)\models\varphi_{reach}$.

In other words, the patched version $P^{\prime}$ should preserve the expected
behavior of $P$, and it should terminate.

###  V-A Termination Bugs in Sequential Programs

To repair termination bugs in sequential programs, we first generate plausible
patches, and then use termination provers to check the correctness of these
patches. AProVE [10] and 2LS [11] are among the most reliable candidates to
analyze the termination of sequential programs.

######  Definition 12 (Validity of Patches for Termination Bugs in Sequential
Programs)

Let $P_{s}$ be a non-terminating sequential program and $T=(T_{p}\cup T_{f})$
be a test-suite consisting of passing test cases $T_{p}$ and failing test
cases $T_{f}$. Let $P^{\prime}_{s}$ be a candidate patch of $P_{s}$ and TP be
a termination prover that returns one of the verification answers
$\\{\text{\emph{TR}},\text{\emph{NT}},\text{\emph{UN}}\\}$. We say that
$P^{\prime}_{s}$ is a valid patch of $P_{s}$ iff all of the following
conditions hold:

  1. 1.

all failing test cases from $T_{f}$ pass on program $P^{\prime}_{s}$,

  2. 2.

none of the passing test cases from $T_{p}$ fail on program $P^{\prime}_{s}$,

  3. 3.

termination prover TP returns “TR” when analyzing termination of
$P^{\prime}_{s}$.

The soundness of generated patches for termination bugs in sequential programs
can be captured formally as:

$\varphi_{\text{\emph{seq}}}=(\forall_{t\in T}(P^{\prime}_{s}\vdash
t)\land\text{\emph{TP}}(P^{\prime}_{s})=\text{\emph{TR}})$ (1)

where $T$ is the set of available test cases, and $P^{\prime}_{s}\vdash t$
indicates that patch $P^{\prime}_{s}$ runs successfully against test $t$.

Figure 1 sketches a hybrid repair procedure for termination bugs in sequential
programs. The algorithm takes five inputs: the buggy sequential program
$P_{s}$, a specification of expected behavior $\varphi_{\text{\emph{beh}}}$, a
test suite $T_{s}$, a termination prover TP, and the allocated time budget
TimeBudget. It uses two functions: (i)
$\text{\emph{faultLocalizer}}(P_{s},\text{\emph{CE}},T_{s})$ computes the set
of suspicious statements SuspStats whose mutation may lead to generate a valid
patch. It finds these suspicious statements by combining the counterexamples
CE generated by termination prover TP with the results of spectrum-based fault
localization [66, 67, 68, 69] on the test suite (executed with a timeout
mechanism to avoid getting stuck in infinite loops); (ii) the function
$\text{\emph{mutate}}(P_{s},\text{\emph{SuspStats}})$ is used to construct the
patch space (i.e., patch generation) by mutating the computed set SuspStats
that may affect the truth value of the termination condition of the detected
buggy non-terminating loop in $P_{s}$.

1:Inputs:
$P_{s},~{}\varphi_{beh},~{}T_{s},~{}\text{\emph{TP}},~{}\text{\emph{TimeBudget}}$

2:Output: $P_{\text{\emph{repaired}}}$

3:$\text{\emph{PatchSpace}}:=\emptyset,~{}P_{\text{\emph{repaired}}}:=\text{\emph{NoPatchFound}},~{}\text{\emph{found}}:=\text{\emph{false}}$

4:$(*,\text{\emph{CE}}):=\text{\emph{TP}}(P_{s})$ # get CE, verdict known to
be NT

5:$\text{\emph{SuspStats}}:=\text{\emph{faultLocalizer}}(P_{s},\text{\emph{CE}},T_{s})$

6:$\text{\emph{PatchSpace}}:=\text{\emph{mutate}}(P_{s},\text{\emph{SuspStats}})$
# patch generation

7:while
$\text{\emph{PatchSpace}}\neq\emptyset\land\text{\emph{TimeBudget}}>0\land\neg\text{\emph{found}}$
do

8: select patch from PatchSpace

9: if $\text{\emph{patch}}\models\varphi_{beh}$ then # 2-step patch validation

10: if $\text{\emph{TP}}(\text{\emph{patch}})=(\text{\emph{TR}},*)$ then

11: $P_{\text{\emph{repaired}}}:=\text{\emph{patch}}$

12: $\text{\emph{found}}:=\text{\emph{true}}$

13: end if

14: end if

15:end while

16:return $P_{\text{\emph{repaired}}}$

Figure 1: Repair algorithm for sequential programs

###  V-B Termination Bugs in Concurrent Programs

In the automated repair of concurrent programs, the goal is to generate a
patch that ensures that a concurrent program is correct under all
interleavings. It is difficult, if not impossible, to examine all possible
executions of a concurrent program using dynamic analysis techniques.
Therefore, a concurrent program cannot be debugged and repaired in the same
manner as sequential programs. In the case of concurrency, it usually refers
to action interleaving. That is, if the processes $p_{i}$ and $p_{j}$ are in
parallel composition ($p_{i}\parallel p_{j}$) then the actions of these will
be interleaved. Each process executes a sequence of actions (sub-program),
then the set of possible interleavings of several processes consists of all
possible sequences of actions. Before proceeding further, let us introduce the
notion of successful termination in concurrent programs.

######  Definition 13 (Termination of Concurrent Programs)

Let $P_{c}=(p_{1}\parallel p_{2}\parallel...\parallel p_{n})$ be a concurrent
program that consists of a collection of sub-programs, where each process
$p_{i}$ executes a sub-program. Let $H_{i}$ be the set of halting statements
at the sub-program executed by process $p_{i}$. We say that $P_{c}$ is
terminating iff every sub-program is eventually terminating. That is, the sub-
program executed by process $p_{i}$ eventually executes some halting statement
$s\in H_{i}$ and terminates.

######  Definition 14 (Termination Failures in Concurrent Programs)

Let $P_{c}=(p_{1}\parallel p_{2}\parallel...\parallel p_{n})$ be a concurrent
program that consists of a collection of sub-programs executed by processes
$p_{1},...,p_{n}$. The program $P_{c}$ fails to terminate iff:

  1. 1.

there exists a logical bug that leads to an infinite loop, or

  2. 2.

there exists a concurrency bug, such as deadlock or livelock, that prevents
the program from making any further progress to reach a halting statement and
terminate.

Thus, if deadlocks and livelocks are formally proven to never occur in the
program-under-analysis, and all loops in the sub-programs are proven to be
terminating, then one can conclude that the concurrent program is terminating.
The distinction between the two causes of termination failures in concurrent
programs (logical bug or concurrency bug) helps to select a strategy for
fixing the detected termination bug.

Combining Model Checking and Termination Provers: Repairing termination bugs
in concurrent programs can be a computationally complex task. This is mainly
because termination bugs in concurrent programs can be caused by either a
logical or concurrency bug. Furthermore, the vast number of possible
interleavings of parallel processes of a given concurrent program can increase
the complexity of the repair problem. Therefore, it is necessary to employ
both termination provers and model checking to reduce the computational
complexity of the problem. Fortunately, we know how to write specifications to
check the absence of concurrency bugs in concurrent programs [70, 71, 72]. In
Definition 15, we describe the conditions that are necessary to ensure the
correctness of the generated patches for termination bugs in the buggy non-
terminating concurrent program.

######  Definition 15 (Validity of Generated Patches for Termination Bugs in
Concurrent Programs)

Let $P_{c}=(p_{1}\parallel p_{2}\parallel...\parallel p_{n})$ be a buggy non-
terminating concurrent program, TP be a termination prover, and SMC be a
software model checker. Let $\varphi_{\text{\emph{deadlock}}}$ and
$\varphi_{\text{\emph{livelock}}}$ be specifications that check respectively
the absence of deadlocks and livelocks in $P_{c}$ and
$\varphi_{\text{\emph{beh}}}$ be a specification that captures the expected
behavior of $P_{c}$. We say that a candidate patch $P^{\prime}_{c}$ for the
buggy program $P_{c}$ is a valid patch iff it meets the following
requirements:

  1. 1.

the prover TP returns “terminating” when analysing termination of the sub-
program executed by process $p_{i}$, and

  2. 2.

the checker SMC returns “holds” when checking the specifications
$\varphi_{\text{\emph{deadlock}}}$ and $\varphi_{\text{\emph{livelock}}}$
against $P^{\prime}_{c}$, and

  3. 3.

the checker SMC returns “holds” when checking the specification of expected
behavior $\varphi_{\text{\emph{beh}}}$ against the patch $P^{\prime}_{c}$.

Formally, we can capture the above described requirements in a 4-part
correctness specification of the following form:

$\begin{array}[t]{l}\varphi_{\text{\emph{con}}}=\forall_{p_{i}\in
P^{\prime}_{c}}(\text{\emph{TP}}(p_{i})=\text{\emph{TR}})\land\text{\emph{SMC}}(P^{\prime}_{c},\varphi_{\text{\emph{deadlock}}})~{}\land\\\
\hskip
41.0pt\text{\emph{SMC}}(P^{\prime}_{c},\varphi_{\text{\emph{livelock}}})\land\text{\emph{SMC}}(P^{\prime}_{c},\varphi_{\text{\emph{beh}}})\end{array}$
(2)

A key challenge when dealing with termination bugs is to ensure that the
generated repair guarantees not only the termination of the program for each
possible input, but also the semantic preservation of the program. This
requires the analysis of a composite correctness property that checks both
termination and semantic preservation. By using formula (2), we entirely avoid
the patch overfitting problem, which is one of the major problems of dynamic
APR. Formula (2) uses sequential termination provers to check the absence of
infinite loops in each individual process. This can be performed while
abstracting away concurrency details that are irrelevant to the local
computations of processes. Note that one cannot prove the termination of
program $P_{c}$ by simply applying a sequential termination prover: a sound
proof of termination must consider all possible interactions among the sub-
programs of $P_{c}$.

An alternative way to use model checking in detecting and repairing
termination bugs of the concurrent program is to reduce the termination
problem to the reachability analysis problem. That is, to check whether each
process will eventually reach some halting location and terminate. However,
the feasibility of the approach relies mainly on the size and number of
processes of the buggy program under analysis (i.e., computing state-
reachability is known to be PSPACE-complete when processes are finite state
[73]). The reduction of the termination problem to the reachability problem in
model checking leads to the following temporal formula

$\varphi_{\text{\emph{con}}}^{\prime}=\forall_{p_{i}\in
P^{\prime}_{c}}(\textbf{AF}(p_{i}.\ell_{h}^{(j)}\mid\ell_{h}^{(j)}\in
H_{i}))\land\text{\emph{SMC}}(P^{\prime}_{c},\varphi_{\text{\emph{beh}}})$ (3)

where A is a temporal path quantifier which should be read as “for all paths”,
and F is the “future” temporal operator [28]. Intuitively, formula (3) checks
whether for each reachable execution path of process $p_{i}$, some halting
location $\ell_{h}^{(j)}\in H_{i}$ will eventually be reached. However, the
proper termination analysis of the concurrent program $P_{c}$ using formula
(3) requires the precise computation of the set of halting locations $H_{i}$
for each process $p_{i}$ of the patched concurrent program $P^{\prime}_{c}$.

There are several software model checkers111 Unlike traditional model
checking, a software model checker does not require a user to manually
construct an abstract model of the program to be checked, but instead, the
tool works directly on the program’s source code. that can be used to verify
reachability properties and detect concurrency bugs, including VeriSoft [14],
Java Pathfinder [16], CMC [17], DIVINE [19], and GMC [74]. DIVINE is a modern,
explicit-state model checker that can verify programs written in multiple
real-world programming languages, including C and C++. On the other hand, GMC
is a model checker based on the generic Monte-Carlo model-checking algorithm.
It takes as input a C program, the target program to be verified, and the
linear temporal logic specification that needs to be checked.

There are also a few termination provers that can be used to analyze the
termination of concurrent programs. For instance, Cook et al. [75] have
extended the termination prover T2 [12] to support the analysis of concurrent
programs, which can be used to validate generated patches for termination bugs
in concurrent programs. Termination checker T2 supports nested loops,
recursive functions, pointers, side-effects, and function-pointers, as well as
concurrent programs. Of course, the prover cannot handle termination of all
concurrent programs since the general problem is undecidable. The use of
concurrent termination provers leads to the following specification

$\varphi_{\text{\emph{con}}}^{\prime\prime}=\forall_{p_{i}\in
P^{\prime}_{c}}(\text{\emph{TP}}(p_{i})=\text{\emph{TR}})\land\text{\emph{SMC}}(P^{\prime}_{c},\varphi_{\text{\emph{beh}}})$
(4)

The termination provers AProVE, 2LS, and T2 can be viewed as complementary
tools: it is possible that some tool fails to detect certain forms of
termination bugs while other succeeds, depending on the implemented theory and
the complexity of the program under analysis. Therefore, termination checkers
can be run in parallel to expose termination bugs.

While checking the satisfaction of formula (2) may require higher
computational complexity than formulas (3) and (4) (i.e., it employs both
termination provers and software model checkers to check the absence of
deadlocks, livelocks, and infinite loops), it has several advantages. First,
it helps identify the root causes of non-termination in the program-under-
repair. Second, the patch validation approach that uses formula (2) can
benefit from the counterexamples generated by both termination provers and
software model checkers. This helps to develop effective program synthesis for
termination bugs.

Repairing Termination Bugs in Concurrent Programs: To fix termination bugs in
concurrent programs, it is first essential to identify the root cause of the
termination bug since both logical and concurrency bugs can cause non-
termination. On the one hand, there are several mechanisms for handling
deadlocks in concurrent programs [71, 72, 76]. On the other, repair algorithms
based on genetic programming can help fix termination bugs that occur due to
infinite loops [45, 77].

Figure 2 sketches a hybrid repair procedure for termination bugs in concurrent
programs. It uses three helper functions: (i)
$\text{\emph{faultLocalizer}}(P_{c},\text{\emph{CE}})$ finds the statements
that are suspected to be faulty in $P_{c}$ using the counterexamples CE
generated by termination prover TP and software model checker SMC, (ii)
$\text{\emph{mutateConcur}}(P_{c},\text{\emph{SuspStatsD}})$ constructs the
patch space for a concurrency bug by mutating the synchronization primitives
of the program, and (iii)
$\text{\emph{mutateLogic}}(P_{c},\text{\emph{SuspStatsL}})$ constructs the
patch space for a logical bug by mutating expressions that affect the control
of faulty loops.

TABLE III: A comparison of the complexity of the repair problem of termination
bugs in sequential and concurrent programs

program class | root causes of non-termination | feasible APR | patch validation procedure | patch validation tools
---|---|---|---|---
sequential programs | infinite loops | dynamic-static | test cases and termination provers | AProVE, 2LS, T2, and GMC
concurrent programs | infinite loops, deadlocks, or livelocks | static or formal | termination provers and SMC | T2 and GMC

1:Inputs:
$P_{c},~{}\varphi_{\text{\emph{beh}}},~{}\varphi_{\text{\emph{deadlock}}},~{}\text{\emph{TP}},~{}\text{\emph{SMC}},~{}\text{\emph{TimeBudget}}$

2:Output: $P_{\text{\emph{repaired}}}$

3:$\text{\emph{PatchSpace}}:=\emptyset,~{}P_{\text{\emph{repaired}}}:=\text{\emph{NoPatchFound}}$,
found := false

4:$(\text{\emph{Outcome}}_{1},\text{\emph{CE}}_{1}):=\text{\emph{SMC}}(P_{c},\varphi_{\text{\emph{deadlock}}})$

5:if $(\text{\emph{Outcome}}_{1}=\text{\emph{fails}}$) then # $P_{c}$ contains
a deadlock

6:
$\text{\emph{SuspStatsD}}:=\text{\emph{faultLocalizer}}(P_{s},\text{\emph{CE}}_{1})$

7: $\text{\emph{PatchSpace}}:=\text{\emph{mutateConcur}}(P_{c},SuspStatsD)$

8:end if

9:$(\text{\emph{Outcome}}_{2},\text{\emph{CE}}_{2}):=\text{\emph{TP}}(P_{c})$

10:if $\text{\emph{Outcome}}_{2}=\text{\emph{NT}}$ then # $P_{c}$ contains an
infinite loop

11:
$\text{\emph{SuspStatsL}}:=\text{\emph{faultLocalizer}}(P_{s},\text{\emph{CE}}_{2})$

12:
$\text{\emph{PatchSpace}}:=\text{\emph{PatchSpace}}\cup\text{\emph{mutateLogic}}(P_{c},\text{\emph{SuspStatsL}})$

13:end if

14:while
$\text{\emph{PatchSpace}}\neq\emptyset\land\text{\emph{TimeBudget}}>0\land\neg\text{\emph{found}}$
do

15: select patch from PatchSpace

16: if $\text{\emph{patch}}\models\varphi_{\text{\emph{beh}}}$ then # 2-step
patch validation

17: if
$\text{\emph{TP}}(\text{\emph{patch}})=(\text{\emph{TR}},*)\land\newline
\hskip
35.56593pt\text{\emph{SMC}}(\text{\emph{patch}},\varphi_{\text{\emph{deadlock}}})=(\text{\emph{holds}},*)$
then

18: $P_{\text{\emph{repaired}}}:=\text{\emph{patch}}$,
$\text{\emph{found}}:=\text{\emph{true}}$

19: end if

20: end if

21:end while

22:return $P_{\text{\emph{repaired}}}$

Figure 2: Repair algorithm for concurrent programs

Generating verified repairs of termination bugs in both sequential and
concurrent programs is a challenging open problem that requires formal
analysis techniques. Our preliminary investigation of using termination
provers in sequential programs shows that this is a rather promising approach
that can be effectively integrated with dynamic APR approaches to generate
verified repairs for termination bugs. The application of the termination
provers 2LS and AProVE on the programs in the two datasets, SNU real-time
benchmark and the Power-Stone benchmark suite [78], show that the tools are
able to successfully prove termination of around $85\%$ of the examined
programs using very little computational time (a few seconds). This
demonstrates the feasibility of using termination provers to validate the
generated patches of termination bugs.

Table III compares the complexity of termination bugs in both sequential and
concurrent programs using several criteria: (i) root causes of termination
bugs, (ii) feasible APR approach to be applied for termination bugs in both
classes of programs, (iii) patch validation procedure to validate generated
patches, (iv) patch validation tool that can be used to check termination.

##  VI Related Work

We discuss the related literature on APR, bug classification, use of formal
specifications in APR, previous attempts to integrate different analysis
techniques, and termination analysis.

Automated Program Repair: Source-based, automated program repair approaches
[3] can be separated into search-based and semantic-based approaches. _Search-
based_ approaches such as GenProg [45], Astor [79], and SCRepair [77]
predominantly use failing test cases to identify bugs, and then mutate the
source code until the program passes all failing test cases. They do not
provide patch correctness guarantees beyond the fact that the provided test
cases now pass. Recent work introduced property-based testing to strengthen
the validation of candidate repairs and address overfitting [80].
Nevertheless, these approaches require executing the program-under-repair,
first to find the bug, and then to generate and validate candidate repairs.
_Semantic-based_ approaches like SemFix [81], Nopol [82], DirectFix [83], SPR
[84], Angelix [85], and JFIX [86] infer repair constraints for the buggy
program via symbolic execution of the given tests. The completeness of
inferred constraints relies on the available test suite. Similarly, Infinitel
[54] uses an SMT solver to synthesise a loop termination condition and then
uses test cases for patch validation.

Bug Classification Systems: Several works target bug classification using a
wide variety of classification criteria and for different goals. The work of
Tan et al. [6, 7] introduced a bug classification system based on the cause-
impact criteria. They studied bug characteristics of around 2,060 real-world
bugs in three representative open-source projects. They concluded that
semantic bugs are the dominant root cause of bugs, and memory-related bugs
have decreased due to the development of effective detection tools. Many bug
tracking systems classify bugs using severity and priority criteria, where
severity indicates the seriousness of the bug on the program functionality and
priority indicates how soon the bug should be fixed [8]. Cotroneo et al.
present a maintenance-oriented bug classification system in which the
characteristics of the bug manifestation are studied [9]. The study identifies
the set of failure-exposing conditions under which a bug may occur. Neither of
these classification systems considers properties that can be used to analyze
the detection power of different bug detection techniques and the conditions
under which they can be integrated, which we add with the classification
system proposed in this paper. Abbaspour et al. [87] do use bug observability
to study the erroneous behavior of a wide variety of concurrency bugs.
However, the authors restrict themselves to concurrency bugs and do not study
the detection power of different bug detection techniques.

Integrating Bug Detection Techniques: Few attempts have been made to integrate
different program analysis techniques to alleviate the impact of the patch
overfitting problem. Al-Bataineh et al. used the static detection
patterns/rules as the source for formulating formal specifications and
discussed the possibility of integrating static and dynamic analysis
techniques to improve the overall quality of generated patches [47]. There
also exists a few examples of using information from debugging to aid APR:
Facebook’s APR tool SapFix takes information generated during the bug
detection process and applies various techniques, including templates specific
to given bug types, to fix the program [4].

Termination Analysis of Programs: A huge body of work has been published on
proving termination of programs based on a variety of techniques, such as
abstract interpretation [55, 58, 59], bounds analysis [60, 61], ranking
functions [62, 63], recurrence sets [64, 65], and transition invariants [56,
57]. Based on these techniques, a number of program termination checkers have
been developed in the prior literature including AProVE [10], 2LS [11], T2
[12], and ARMC [88]. Unfortunately, termination provers have not yet been used
to _validate_ the generated candidate patches of termination bugs in the
previous APR approaches. We strongly believe that integrating APR approaches
with contemporary termination checkers would help advance the current state-
of-the-art of APR, not only for repairing termination bugs, but also for other
classes of concurrency bugs. This is mainly because fixing termination bugs in
concurrent programs would ensure the absence of certain classes of concurrency
bugs, such as deadlock and livelock bugs. It would also help avoid the patch
overfitting problem by generating verified repairs for termination bugs in
both sequential and concurrent programs.

##  VII Concluding Remarks

A significant class of bugs cannot be handled with current APR approaches, and
there is a need to study complementary techniques. To stimulate this work, we
propose a novel bug classification system based on three key properties: bug
observability, bug tractability, and bug reproducibility. This provides a tool
to methodologically explore and compare alternative and hybrid APR approaches
by (i) analyzing the detection power of different bug detection techniques,
(ii) distinguishing APR approaches based on their bug repair capabilities, and
(iii) providing a common terminology that helps identify gaps in current APR
research. Moreover, it allows analysis of how techniques can be combined to
handle challenging classes of bugs. As a demonstrating example, we study
termination bugs in sequential and concurrent programs, and present novel
_hybrid_ algorithms for their repair by integrating termination provers and
software model checkers in the APR pipeline. Such integration reduces the
complexity of the repair algorithms and improves the overall reliability.

We identify the following directions for future research: (1) we are in the
process of empirically validating the ideas described in this work by
combining a selection of APR tools with some of the termination provers and
software model checkers mentioned earlier; (2) there is a need for efficient
fault localization mechanisms for termination and liveness bugs, since these
create infinite traces that cannot be handled with the current spectrum-based
fault localization approaches; We currently circumvent this with a timeout
mechanism, but more efficient techniques could find a more precise set of
suspicious statements; (3) the combination of CounterExample-Guided Inductive
Synthesis (CEGIS) [89] with termination provers and software model checkers
could enable efficient patch space exploration without the user guidance that
is normally needed for CEGIS; (4) aside from the termination bugs studied in
Section V, various other bugs cannot be handled by APR approaches solely based
on dynamic analysis. One particularly interesting class of non-observable bugs
for future research are security-related vulnerabilities where sensitive
information may be disclosed to unauthorized parties as a result of violations
of information flow security [36, 37].

## References

  * [1] E. Swanson  “The Dimensions of Maintenance”  In _Int’l Conference on Software Engineering (ICSE)_ , ICSE ’76  IEEE, 1976, pp. 492–497
  * [2] Claire Le Goues, Michael Pradel and Abhik Roychoudhury  “Automated Program Repair”  In _Communications of the ACM_ 62.12, 2019, pp. 56–65  DOI: 10/gkgf29
  * [3] Martin Monperrus  “Automatic Software Repair: A Bibliography”  In _ACM Computing Surveys_ 51.1, 2018, pp. 1–24  DOI: 10/ggssbj
  * [4] Alexandru Marginean, Johannes Bader, Satish Chandra, Mark Harman, Yue Jia, Ke Mao, Alexander Mols and Andrew Scott  “SapFix: Automated End-to-End Repair at Scale”  In _Int’l Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)_ , 2019, pp. 269–278  DOI: 10/gkgf2c
  * [5] Bowen Alpern and Fred B. Schneider  “Recognizing Safety and Liveness”  In _Distributed Computing_ 2.3, 1987, pp. 117–126  DOI: 10/fmbptq
  * [6] Zhenmin Li, Lin Tan, Xuanhui Wang, Shan Lu, Yuanyuan Zhou and Chengxiang Zhai  “Have Things Changed Now? An Empirical Study of Bug Characteristics in Modern Open Source Software”  In _Workshop on Architectural and System Support for Improving Software Dependability_ New York, NY, USA: ACM, 2006, pp. 25–33  DOI: 10/cqsw86
  * [7] Lin Tan, Chen Liu, Zhenmin Li, Xuanhui Wang, Yuanyuan Zhou and Chengxiang Zhai  “Bug Characteristics in Open Source Software”  In _Empirical Software Engineering_ 19.6, 2014, pp. 1665–1705  DOI: 10/f6m38x
  * [8] N. Serrano and I. Ciordia  “Bugzilla, ITracker, and Other Bug Trackers”  In _IEEE Software_ 22.2, 2005, pp. 11–13  DOI: 10/fbgs99
  * [9] Domenico Cotroneo, Kishor Trivedib, Stefano Russoa and Roberto Pietrantuonoa  “How Do Bugs Surface? A Comprehensive Study on the Characteristics of Software Bugs Manifestation”  In _Journal of Systems and Software_ 113, 2016, pp. 27–43  DOI: 10/gpd4t5
  * [10] Jürgen Giesl et al.  “Proving Termination of Programs Automatically with AProVE”  In _Int’l Joint Conference on Automated Reasoning (IJCAR)_ Cham: Springer, 2014, pp. 184–191  DOI: 10/f3ssz2
  * [11] Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel and Björn Wachter  “Synthesising Interprocedural Bit-Precise Termination Proofs (T)”  In _Int’l Conference on Automated Software Engineering (ASE)_ , 2015, pp. 53–64  DOI: 10/gp6krb
  * [12] Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf and Nir Piterman  “T2: Temporal Property Verification”  In _Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_ Berlin, Heidelberg: Springer, 2016, pp. 387–393  DOI: 10/gp6kq9
  * [13] Ranjit Jhala and Rupak Majumdar  “Software Model Checking”  In _ACM Computing Surveys_ 41.4, 2009, pp. 1–54  DOI: 10/fd3pxq
  * [14] Patrice Godefroid  “VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software”  In _Int’l Conference on Computer Aided Verification (CAV)_ Berlin, Heidelberg: Springer, 1997, pp. 476–479  DOI: 10/b7ntq3
  * [15] G.J. Holzmann  “The Model Checker SPIN”  In _IEEE Transactions on Software Engineering_ 23.5, 1997, pp. 279–295  DOI: 10/d7wqxt
  * [16] Klaus Havelund and Thomas Pressburger  “Model Checking JAVA Programs Using JAVA PathFinder”  In _International Journal on Software Tools for Technology Transfer_ 2.4, 2000, pp. 366–381  DOI: 10/d2pmx6
  * [17] Madanlal Musuvathi, David Y.. Park, Andy Chou, Dawson R. Engler and David L. Dill  “CMC: A Pragmatic Approach to Model Checking Real Code”  In _Symposium on Operating Systems Design and Implementation (OSDI)_ Usenix, 2002
  * [18] Sarah J Thompson, Guillaume Brat and Arnaud Venet  “Software Model Checking of ARINC-653 Flight Code with MCP”  In _NASA Formal Methods Symposium_ NASA, 2010
  * [19] Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai and Vladimír Štill  “Model Checking of C and C++ with DIVINE 4”  In _Automated Technology for Verification and Analysis_ Cham: Springer, 2017, pp. 201–207  DOI: 10/gp6kq7
  * [20] Yacine Hebbal, Sylvie Laniepce and Jean-Marc Menaud  “Virtual Machine Introspection: Techniques and Applications”  In _Int’l Conference on Availability, Reliability and Security_ , 2015, pp. 676–685  DOI: 10/gp6kq4
  * [21] Pavel Dovgalyuk, Natalia Fursova, Ivan Vasiliev and Vladimir Makarov  “QEMU-based Framework for Non-Intrusive Virtual Machine Instrumentation and Introspection”  In _Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)_ , ESEC/FSE 2017  ACM, 2017, pp. 944–948  DOI: 10/gp6kqz
  * [22] Brendan Gregg  “Systems Performance: Enterprise and the Cloud”, Addison-Wesley Professional Computing Series  Boston: Addison-Wesley, 2020
  * [23] Brendan Gregg  “BPF Performance Tools: Linux System and Application Observability”  Addison-Wesley
  * [24] Omar Al-Bataineh, Daniel Jun Xian Ng and Arvind Easwaran  “Monitoring Cumulative Cost Properties”  In _Int’l Conference on Formal Methods in Software Engineering (FormaliSE)_ , 2021, pp. 19–30  DOI: 10/gp6kqw
  * [25] Todd Mytkowicz, Peter F Sweeney, Matthias Hauswirth and Amer Diwan  “Observer Effect and Measurement Bias in Performance Analysis”, 2008
  * [26] Xi Wang, Zhenyu Guo, Xuezheng Liu, Zhilei Xu, Haoxiang Lin, Xiaoge Wang and Zheng Zhang  “Hang Analysis: Fighting Responsiveness Bugs”  In _ACM SIGOPS Operating Systems Review_ 42.4, 2008, pp. 177–190  DOI: 10/b9chm8
  * [27] Daniel J. Dean, Peipei Wang, Xiaohui Gu, William Enck and Guoliang Jin  “Automatic Server Hang Bug Diagnosis: Feasible Reality or Pipe Dream?”  In _IEEE Int’l Conference on Autonomic Computing_ , 2015, pp. 127–132  DOI: 10/gp6kq5
  * [28] Amir Pnueli  “The Temporal Logic of Programs”  In _Annual Symposium on Foundations of Computer Science (SFCS)_ , 1977, pp. 46–57  DOI: 10/dn8cpn
  * [29] Zohar Manna and Amir Pnueli  “The Temporal Logic of Reactive and Concurrent Systems: Specification”  New York, NY: Springer, 1992
  * [30] L. Lamport  “Proving the Correctness of Multiprocess Programs”  In _IEEE Transactions on Software Engineering_ SE-3.2, 1977, pp. 125–143  DOI: 10/d25dpw
  * [31] Bowen Alpern and Fred B. Schneider  “Defining Liveness”  In _Information Processing Letters_ 21.4, 1985, pp. 181–185  DOI: 10/d97bw4
  * [32] Charles Killian, James W. Anderson, Ranjit Jhala and Amin Vahdat  “Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code”  In _USENIX Symposium on Networked Systems Design & Implementation (NSDI 07)_, 2007
  * [33] Peng Li and John Regehr  “T-Check: Bug Finding for Sensor Networks”  In _Int’l Conference on Information Processing in Sensor Networks_ , IPSN ’10  ACM, 2010, pp. 174–185  DOI: 10/djrwkg
  * [34] Barton P. Miller, Louis Fredriksen and Bryan So  “An Empirical Study of the Reliability of UNIX Utilities”  In _Communications of the ACM_ 33.12, 1990, pp. 32–44  DOI: 10/fqnt9s
  * [35] Barton P. Miller, Gregory Cooksey and Fredrick Moore  “An Empirical Study of the Robustness of MacOS Applications Using Random Testing”  In _Int’l Workshop on Random Testing_ , RT ’06  New York, NY, USA: ACM, 2006, pp. 46–54  DOI: 10/bw7w9h
  * [36] A. Sabelfeld and A.C. Myers  “Language-Based Information-Flow Security”  In _IEEE Journal on Selected Areas in Communications_ 21.1, 2003, pp. 5–19  DOI: 10/dnvjwg
  * [37] Geoffrey Smith  “Principles of Secure Information Flow Analysis”  In _Malware Detection_ Boston, MA: Springer, 2007, pp. 291–307  DOI: 10/fnfjff
  * [38] Cristina David, Pascal Kesseli, Daniel Kroening and Matt Lewis  “Danger Invariants”  In _Formal Methods_ , Lecture Notes in Computer Science  Cham: Springer, 2016, pp. 182–198  DOI: 10/gp6kqr
  * [39] Vijay D’Silva, Daniel Kroening and Georg Weissenbacher  “A Survey of Automated Techniques for Formal Software Verification”  In _IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems_ 27.7, 2008, pp. 1165–1178  DOI: 10/frf7ww
  * [40] Al Bessey et al.  “A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World”  In _Communications of the ACM_ 53.2, 2010, pp. 66–75  DOI: 10/bj8r36
  * [41] Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon and Ciera Jaspan  “Lessons from Building Static Analysis Tools at Google”  In _Communications of the ACM_ 61.4, 2018, pp. 58–66  DOI: 10/ggsshq
  * [42] J.. Burch, E.. Clarke, K.. McMillan, D.. Dill and L.. Hwang  “Symbolic Model Checking: 1020 States and Beyond”  In _Information and Computation_ 98.2, 1992, pp. 142–170  DOI: 10/bvrsx5
  * [43] Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen and Pierre McKenzie  “Systems and Software Verification: Model-Checking Techniques and Tools”  Berlin, Heidelberg: Springer, 2001
  * [44] E.M. Clarke, O. Grumberg, D. Kroening, D. Peled and H. Veith  “Model Checking”, Cyber Physical Systems Series  MIT Press, 2018
  * [45] Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest and Westley Weimer  “GenProg: A Generic Method for Automatic Software Repair”  In _IEEE Transactions on Software Engineering_ 38.1, 2012, pp. 54–72  DOI: 10/cfztf3
  * [46] Paul Muntean, Martin Monperrus, Hao Sun, Jens Grossklags and Claudia Eckert  “IntRepair: Informed Repairing of Integer Overflows”  In _IEEE Transactions on Software Engineering_ 47.10, 2021, pp. 2225–2241  DOI: 10/gh97rm
  * [47] Omar I. Al-Bataineh, Anastasiia Grishina and Leon Moonen  “Towards More Reliable Automated Program Repair by Integrating Static Analysis Techniques”  In _IEEE Int’l Conference on Software Quality, Reliability and Security (QRS)_ , 2021, pp. 654–663  DOI: 10/gp6kq6
  * [48] Guoliang Jin, Linhai Song, Xiaoming Shi, Joel Scherpelz and Shan Lu  “Understanding and Detecting Real-World Performance Bugs”  In _ACM SIGPLAN Notices_ 47.6, 2012, pp. 77–88  DOI: 10/f372jr
  * [49] Aida Radu and Sarah Nadi  “A Dataset of Non-Functional Bugs”  In _Int’l Conference on Mining Software Repositories (MSR)_ Montreal, Quebec, Canada: IEEE, 2019, pp. 399–403  DOI: 10/gp6kq2
  * [50] M.. Fagan  “Design and Code Inspections to Reduce Errors in Program Development”  In _IBM Systems Journal_ 15.3, 1976, pp. 182–211  DOI: 10/btfv3v
  * [51] Tom Gilb, Dorothy Graham and Susannah Finzi  “Software Inspection”  Wokingham, England ; Reading, Mass: Addison-Wesley, 1993
  * [52] Alberto Bacchelli and Christian Bird  “Expectations, Outcomes, and Challenges of Modern Code Review”  In _Int’l Conference on Software Engineering (ICSE)_ , 2013, pp. 712–721  DOI: 10/gf2h2r
  * [53] Claire Le Goues, Neal Holtschulte, Edward K. Smith, Yuriy Brun, Premkumar Devanbu, Stephanie Forrest and Westley Weimer  “The ManyBugs and IntroClass Benchmarks for Automated Repair of C Programs”  In _IEEE Transactions on Software Engineering_ 41.12, 2015, pp. 1236–1256  DOI: 10/gpd4jv
  * [54] Sebastian R. Marcote and Martin Monperrus  “Automatic Repair of Infinite Loops”  arXiv, 2015  DOI: 10/jb2f
  * [55] Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano and Peter O’Hearn  “Variance Analyses from Invariance Analyses”  In _SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_ , POPL ’07  New York, NY, USA: ACM, 2007, pp. 211–224  DOI: 10/frk5km
  * [56] Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich and Christoph M. Wintersteiger  “Termination Analysis with Compositional Transition Invariants”  In _Computer Aided Verification_ Berlin, Heidelberg: Springer, 2010, pp. 89–103  DOI: 10/b54tf5
  * [57] A. Podelski and A. Rybalchenko  “Transition Invariants”  In _Symposium on Logic in Computer Science_ , 2004, pp. 32–41  DOI: 10/fbsbdm
  * [58] Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv and Hongseok Yang  “Ranking Abstractions”  In _European Symposium on Programming Languages and Systems (ESOP)_ Berlin, Heidelberg: Springer, 2008, pp. 148–162  DOI: 10/d4wm5s
  * [59] Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger and Daniel Kroening  “Loop Summarization and Termination Analysis”  In _Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_ Berlin, Heidelberg: Springer, 2011, pp. 81–95  DOI: 10/cd8sdb
  * [60] Sumit Gulwani, Sagar Jain and Eric Koskinen  “Control-Flow Refinement and Progress Invariants for Bound Analysis”  In _ACM SIGPLAN Notices_ 44.6, 2009, pp. 375–385  DOI: 10/fxdmzw
  * [61] Sumit Gulwani, Krishna K. Mehra and Trishul Chilimbi  “SPEED: Precise and Efficient Static Estimation of Program Computational Complexity”  In _ACM SIGPLAN Notices_ 44.1, 2009, pp. 127–139  DOI: 10/fxgdsx
  * [62] Aaron R. Bradley, Zohar Manna and Henny B. Sipma  “Linear Ranking with Reachability”  In _Int’l Conference on Computer Aided Verification (CAV)_ Berlin, Heidelberg: Springer, 2005, pp. 491–504  DOI: 10/fpjv58
  * [63] Patrick Cousot  “Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming”  In _Verification, Model Checking, and Abstract Interpretation_ Berlin, Heidelberg: Springer, 2005, pp. 1–24  DOI: 10/dzfpc6
  * [64] Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko and Ru-Gang Xu  “Proving Non-Termination”  In _SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_ , POPL ’08  New York, NY, USA: ACM, 2008, pp. 147–158  DOI: 10/dd76q5
  * [65] William R. Harris, Akash Lal, Aditya V. Nori and Sriram K. Rajamani  “Alternation for Termination”  In _Static Analysis Symposium (SAS)_ Berlin, Heidelberg: Springer, 2010, pp. 304–319  DOI: 10/djthds
  * [66] James A. Jones, Mary Jean Harrold and John Stasko  “Visualization of Test Information to Assist Fault Localization”  In _Int’l Conference on Software Engineering (ICSE)_ , 2002, pp. 467  DOI: 10/bxz64c
  * [67] Lee Naish, Hua Jie Lee and Kotagiri Ramamohanarao  “A Model for Spectra-Based Software Diagnosis”  In _ACM Transactions on Software Engineering and Methodology (TOSEM)_ 20.3, 2011, pp. 1–32  DOI: 10/c5xnmd
  * [68] Simon Heiden, Lars Grunske, Timo Kehrer, Fabian Keller, Andre Hoorn, Antonio Filieri and David Lo  “An Evaluation of Pure Spectrum-Based Fault Localization Techniques for Large-Scale Software Systems”  In _Software: Practice and Experience_ 49.8, 2019, pp. 1197–1224  DOI: 10/gp6kq8
  * [69] Xiaoyuan Xie and Baowen Xu  “Essential Spectrum-based Fault Localization”  Singapore: Springer, 2021  DOI: 10/jb2d
  * [70] Aarti Gupta, Vineet Kahlon, Shaz Qadeer and Tayssir Touili  “Model Checking Concurrent Programs”  In _Handbook of Model Checking_ Cham: Springer, 2018, pp. 573–611  DOI: 10/jkpx
  * [71] Yiyan Lin and Sandeep S. Kulkarni  “Automatic Repair for Multi-Threaded Programs with Deadlock/Livelock Using Maximum Satisfiability”  In _Int’l Symposium on Software Testing and Analysis (ISSTA)_ , ISSTA 2014  New York, NY, USA: ACM, 2014, pp. 237–247  DOI: 10/gp6krh
  * [72] Jinpeng Zhou, Sam Silvestro, Hongyu Liu, Yan Cai and Tongping Liu  “UNDEAD: Detecting and Preventing Deadlocks in Production Software”  In _Int’l Conference on Automated Software Engineering (ASE)_ , 2017, pp. 729–740  DOI: 10/gp6kqx
  * [73] Dexter Kozen  “Lower Bounds for Natural Proof Systems”  In _Annual Symposium on Foundations of Computer Science (SFCS)_ , 1977, pp. 254–266  DOI: 10/dbkc79
  * [74] S. Thompson and G. Brat  “Verification of C++ Flight Software with the MCP Model Checker”  In _IEEE Aerospace Conference_ Big Sky, MT, USA: IEEE, 2008, pp. 1–9  DOI: 10/ds9chc
  * [75] Byron Cook, Andreas Podelski and Andrey Rybalchenko  “Proving Thread Termination”  In _Conference on Programming Language Design and Implementation (PLDI)_ , PLDI ’07  New York, NY, USA: ACM, 2007, pp. 320–330  DOI: 10/dp236p
  * [76] Yan Cai and Lingwei Cao  “Fixing Deadlocks via Lock Pre-Acquisitions”  In _Int’l Conference on Software Engineering (ICSE)_ , ICSE ’16  New York, NY, USA: ACM, 2016, pp. 1109–1120  DOI: 10/gp6kq3
  * [77] Xiao Liang Yu, Omar Al-Bataineh, David Lo and Abhik Roychoudhury  “Smart Contract Repair”  In _ACM Transactions on Software Engineering and Methodology_ 29.4, 2020, pp. 1–32  DOI: 10/gpd4hr
  * [78] Kelvin Ku, Thomas E. Hart, Marsha Chechik and David Lie  “A Buffer Overflow Benchmark for Software Model Checkers”  In _Int’l Conference on Automated Software Engineering (ASE)_ , ASE ’07  New York, NY, USA: ACM, 2007, pp. 389–392  DOI: 10/fds27b
  * [79] Matias Martinez and Martin Monperrus  “ASTOR: A Program Repair Library for Java”  In _Int’l Symposium on Software Testing and Analysis (ISSTA)_ Saarbrücken Germany: ACM, 2016, pp. 441–444  DOI: 10/gndn55
  * [80] Matthias Páll Gissurarson, Leonhard Applis, Annibale Panichella, Arie van Deursen and David Sands  “PROPR: Property-Based Automatic Program Repair”  In _Int’l Conference on Software Engineering (ICSE)_ , 2022, pp. 1768–1780  DOI: 10/gqhgs7
  * [81] Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury and Satish Chandra  “SemFix: Program Repair via Semantic Analysis”  In _Int’l Conference on Software Engineering (ICSE)_ , 2013, pp. 772–781  DOI: 10/gg82z6
  * [82] Jifeng Xuan, Matias Martinez, Favio DeMarco, Maxime Clément, Sebastian Lamelas Marcote, Thomas Durieux, Daniel Le Berre and Martin Monperrus  “Nopol: Automatic Repair of Conditional Statement Bugs in Java Programs”  In _IEEE Transactions on Software Engineering_ 43.1, 2017, pp. 34–55  DOI: 10/gm5s3h
  * [83] Sergey Mechtaev, Jooyong Yi and Abhik Roychoudhury  “DirectFix: Looking for Simple Program Repairs”  In _Int’l Conference on Software Engineering (ICSE)_ 1, 2015, pp. 448–458  DOI: 10/gndpcr
  * [84] Fan Long and Martin Rinard  “Staged Program Repair with Condition Synthesis”  In _Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)_ , ESEC/FSE 2015  New York, NY, USA: ACM, 2015, pp. 166–178  DOI: 10/gfvmzm
  * [85] Sergey Mechtaev, Jooyong Yi and Abhik Roychoudhury  “Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis”  In _Int’l Conference on Software Engineering (ICSE)_ , 2016, pp. 691–701  DOI: 10/ggsskp
  * [86] Xuan-Bach D. Le, Duc-Hiep Chu, David Lo, Claire Le Goues and Willem Visser  “JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder”  In _Int’l Symposium on Software Testing and Analysis (ISSTA)_ , ISSTA 2017  New York, NY, USA: ACM, 2017, pp. 376–379  DOI: 10/gp6krg
  * [87] Sara Abbaspour Asadollah, Hans Hansson, Daniel Sundmark and Sigrid Eldh  “Towards Classification of Concurrency Bugs Based on Observable Properties”  In _Int’l Workshop on Complex Faults and Failures in Large Software Systems (COUFLESS)_ , 2015, pp. 41–47  DOI: 10/f3nh6c
  * [88] Andreas Podelski and Andrey Rybalchenko  “ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement”  In _Practical Aspects of Declarative Languages_ Berlin, Heidelberg: Springer, 2007, pp. 245–259  DOI: 10/dmrfmf
  * [89] Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia and Vijay Saraswat  “Combinatorial Sketching for Finite Programs”  In _Int’l Conference on Architectural Support for Programming Languages and Operating Systems_ , ASPLOS XII  New York, NY, USA: ACM, 2006, pp. 404–415  DOI: 10/fdsnnt