On the Integration of Software Testing and Formal Analysis - Empirical Software Engineering and Verification - page 183

Static/dynamic verification. The static/dynamic verification approach Dash re-
cently introduced by Beckman et al. computes the reachability of (faulty) state-
ments of programs [3]. Given a program p and a target statement in p , Dash
searches for either a test case that executes the target statement, or a proof
that such statement is unreachable in p . Dash searches for a test case that
executes the target statement by exploring program paths increasingly closer
to it, by means of directed testing. It tries to prove that the target statement
is unreachable by progressively refining a finite abstract model that conserva-
tively overapproximates all transitions between the program statements, until
the model eventually contains no abstract trace that includes the target state-
ment. The two searches interplay as Dash stores the abstract states supported
by the concrete states generated by testing, and uses such information to direct
and coordinate test case generation and model refinement.
Dash initially assumes an abstract model equivalent to the static control flow
graph of the program, and generates a random test case. Then Dash iterates
through the following steps until either the target statement becomes unreach-
able in the current abstract model, or it is executed by a test case. Dash identifies
a frontier transition within the abstract model, i.e. a transition that belongs to
some abstract trace that goes from the program entry to the target statement 9 ,
and connects the last abstract state σ 1 covered by at least a test case t ,tothe
first abstract state σ 2 not covered by any test case. Next, it executes t concol-
ically up to state σ 1 , augments the obtained path condition with the clause to
cross the frontier to σ 2 , and checks for its satisfiability with an automatic solver.
A solution, when found by the solver, is a new test case that covers σ 2 ,thus
progressing in the search for a feasible path towards the target statement. If
the solver does not find a solution, Dash eliminates the infeasible abstract trace
from the model by conservatively refining σ 1 along the frontier transition.
Figure 12 illustrates how Dash refines the model (Figure 12 (b)), given a
frontier transition from an abstract state σ 1 covered by a concrete state s to
a state σ 2 (Figure 12 (a)). From the definition of frontier it follows that σ 1
is supported by a concrete state s generated by a test t , σ 2 is not supported
by any concrete state, and no state reaching σ 1 along t can reach σ 2 . Dash
splits σ 1 into two new states annotated with refinement predicates r and its
negation respectively 10 . The predicate r is satisfied by all the concrete states
that may have a post-state in σ 2 ,thus ¬r is satisfied by all the concrete states
that have no post-states in σ 2 (including s ) 11 .Consequently, σ 2 may be reachable
from the region with extension r ∧ σ 1 , but not from the region with extension

¬ r ∧ σ 1 . This sets the frontier one step backwards, and the problem of proving

9 Such a transition is guaranteed to exist, until the termination conditions are not
met.
10 Note that, if a frontier state σ 2 includes a refinement predicate, Dash can generate
a test case that satisfy it. For this reason, concolic execution adds the refinement
predicate of σ 2 to the current path condition.
11 When the program is deterministic, every concrete state that supports σ 1 must sat-
isfy ¬r : otherwise, its only possible successor would support σ 2 thatis not supported

by the definition of frontier.