Information Technology Reference
In-Depth Information
information should they share to interplay? How does this interplay improve
precision, convergence or performance? How can we design a combination be-
tween techniques in a way that yields a predictable advantage? How can we
discover new combination patterns? Giving an answer to some of these ques-
tions can highlight the commonalities among different combined techniques and
can provide the foundations for new tools for designing better testing, analysis
and verification techniques.
This paper moves a first step in the direction of answering some of the above
questions. We propose a vocabulary of concepts which, in our vision, allow to
motivate, understand and evaluate the interactions between static and dynamic
techniques. These concepts are grounded on a definition of technique as a way
to explore the reachable state space of a program, and will characterize differ-
ent techniques in terms of how they restrict the ideal but infeasible exhaustive
exploration to make exploration feasible. The framework allows us to motivate
and explain a number of combination patterns between techniques emerging
from current literature. We assess the advantage of these combination patterns
informally, and we propose some preliminary ideas about a more quantitative
assessment. All these concepts are grounded on current research by considering
some state-of-the-research static/dynamic tools as case studies and guides for
identifying the combination patterns.
The paper is organized as follows. Section 2 defines the category of programs,
analysis problems and techniques that are considered in the rest of the paper.
Section 3 introduces and classifies basic state space exploration techniques, on
which combined approaches are based, with a special attention to testing, sym-
bolic execution and predicate abstraction. Section 4 introduces the concept of
synergies between techniques, as the way techniques exchange information about
the program state space, identifies a set of synergies that recur across three repre-
sentative combined techniques from literature, and discusses their aims in terms
of improved performance or completeness. Section 5 considers the problem of
assessing in a more quantitative way how combined techniques improve over
purely static or dynamic ones, and calculates the performance gain that derives
form a specific synergy pattern, by isolating its effect in two combined techniques
among those surveyed in Section 4. Finally, Section 6 draws some conclusions
and outlines an agenda for future research.
2 Preliminaries: Programs, Properties and Analysis
This section sets the scope of the paper and introduces some preliminary defi-
nitions that will be used in the next sections: What do we consider as software
programs, which category of correctness problems are we dealing with, what is
a technique for analyzing the program correctness.
2.1 Programs
We consider software systems written in an imperative programming language.
An imperative program transforms an initial program state into a final one.
 
Search WWH ::




Custom Search