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

ExploreBallYorshSagiv( p , I , O , A ):
S S A := S A I ⊆

:= ;

loop:
if S ⊆ O return INCONCLUSIVE
S := Post( p, S ) ⊆
if

S ⊆ S :

φ := sp( p, φ ) φ S A

:= ;

φ = ⇒ φ

if return CORRECT

S := φ ∧¬φ ⊆

S A S A

:=

S − S S A S A S S A

:= ; :=

Fig. 11. Yorsh-Ball-Sagiv procedure

a feeding of reachable states (FRS) and a frontier abduction (FA) approach, as
illustrated by the formulas:

S A := S A ; S A := S A S A ,

and:

S := φ ∧¬ ⊆ ; S := S − S.

The frontier is built by symbolically analyzing the abstract region S A ,which
(trivially) constrains symbolic execution by the statement:

φ

; φ := sp( p, φ ) . φ := S A

In general, the Yorsh-Ball-Sagiv procedure converges when the height of the
lattice of abstract program properties is finite, as in the case of predicate ab-
straction. When the height of the lattice is finite and the procedure is adequately
supported by a theorem prover and a solver, the Yorsh-Ball-Sagiv procedure
computes an abstract property that covers as many states as the most-precise
(i.e., existential) abstract interpreter.
The readers should notice that the concrete states computed by checking
invariance are not necessarily reachable program states, and this is in line with
the over-approximation of the most-precise abstract interpreter. The more the
abstract states discovered by concrete execution, the more the Yorsh-Ball-
Sagiv procedure is ecient with respect to a completely static approach like
the predicate abstraction approach illustrated in Figures 8 and 9. The Yorsh-
Ball-Sagiv procedure improves on speed, while maintaining the same precision.
We discuss this point in detail in Section 5.
We conclude with a final remark that apply to both the Yorsh-Ball-Sagiv
procedure and concolic execution: The invariance check and frontier abduction
consider, essentially, the same predicates. Both problems are tantamount to de-
ciding whether the predicate φ ∧¬

φ has at least a solution. When we can find
a solution, it is an abduced frontier, since it ensures progress towards a yet
uncovered abstract state, that can be added to S A .