ソフトウェア・シンポジウム 2023 in 仙台

Testing-Based Formal Verification on Software Programs: A Review
Ai LiuHiroshima University
liuai@hiroshima-u.ac.jp

Abstract
Testing-based formal verification has been proposed to automatically verify whether a software
program satisfies the requirements written as aformal specification by exploring program paths.
There are two tools that can be used to verify
path correctness: Hoare logic or symbolic execution. In this document, we will discuss their merits and demerits, as well as the future research
directions.

1. Introduction
Software testing, one of the most frequently used
quality assurance methods, is focused on sampling theexecutions, according to some coverage criteria, andcomparing the actual behavior with the expected behavior. Nevertheless, a typical weakness of testing isthat it cannot generally tell the absence of bugs in programs. To find more bugs, more test data need to begenerated and more program executions, which will inevitably increasing the cost. An idea for improvement
is to ensure the correctness of the executed path fora given test case with formal methods and then all of
the test cases, resulting in the same executed path, will
satisfy the expected behavior.
Formal methods, based on some mathematical theories, are a collection of notations and techniques, including specification and verification [1]. Formal specification techniques introduce a precise and unambiguous description of the software behavior. Given sucha specification, it is possible to use formal verification
techniques to demonstrate that a software design is correct with respect to the specification. However, mostof software verification methods do not guarantee thecorrectness of actual code, but rather allow one to verify some abstract model of it. Hence, due to possible
differences between the actual software system and its
abstract model, the correctness of the proof may notcarry over. To ensure the correctness of the code, deductive verification, including symbolic execution andShaoyin Liu
Hiroshima University
sliu@hiroshima-u.ac.jp

Hoare logic, has been demonstrated mainly for simple
programs which contain no loop sentences and no side
effects.
Hoare logic is established based on predicate logic
and provides a set of axioms to define the semantics
of programming language [2]. For each program construct, such as sequence, selection, or iteration, an axiom for defining its semantics is defined. These axioms
can be used to reason about the correctness of programs written in a programming language. However,
the axiom for iteration is hard to be directly used since
the derivation of loop invariants may not be easy.
Symbolic execution systematically explores the possible paths of a program’s execution by executing the
program with symbolic inputs instead of concrete values and then allows the tester to explore different execution paths and detect potential bugs and vulnerabilities [3]. Symbolic execution is often used in combination with other techniques such as model checking andtheorem proving to verify the correctness of softwaresystems. There are severe challenges of symbolic execution such as path explosion and constraint solving.
Nevertheless, it is an active area of research, and newtechniques and tools are constantly being developed to
improve its efficiency and effectiveness.
A natural idea is to combine testing and formal
methods (specification and verification) to make thebest use of their merits while reducing the cost. As
Whittaker noted “Without a specification testers arelikely to find only the most obvious bugs” in 2000,
specification-based testing (SBT) has been advocatedfor a long time [4, 5]. However, due to the weakness of testing to tell the absence of bugs in programs,
specification-based testing also need high test cost inorder to improve software reliability. For the purpose
to improve specification-based testing with formal verification techniques, a method known as testing-basedformal verification (TBFV), characterized by the integration of specification-based testing with Hoare logic
to ensure the correctness of program paths which contain no loop sentences and no side effects, has been ex-

38

SEA

ソフトウェア・シンポジウム 2023 in 仙台

plored and its initial idea is proposed in [6]. The idea isfurther developed to combine with program inspection
later [7]. A collection of prototype tools to illustrate
how to support the TBFV method is presented in [8].
The original framework of TBFV is extended in [9] todeal with operations, which may involve with complex
data structure and side effects, in software packages,
such as Vector, ArrayList and LinkedList packages inJava language. Before that extension, testing-basedformal verification with symbolic execution is alternatively proposed as an improved method by replacing
the application of Hoare logic with symbolic execution
in [10]. Branch sequence coverage (BSC) for TBFV-SE
is considered in [11] and a fault localization approach is
proposed to further pinpoint the problematic positionsin the incorrect program paths given by TBFV-SE in[12]. Moreover, the idea is also applied to the verification of neural networks, resulting in TBFV-INN, a newframework for verifying and improving neural networks[13].
As previously mentioned, since TBFV is firstly proposed, it has been constantly improved on two roads:
one is based on Hoare logic and the other is based onsymbolic execution. In this document, we will enjoy
different scenery and discuss which treasure we intend
to dig on the two roads in the future.
The rest is organized as follows. Section 2 introduces the framework of testing-based formal verification. Section 3 describes the framework of test-basedformal verification with symbolic execution. Section 4
discusses the merits and demerits of TBFV and TBFVSE.

Generate a test case t satisfying some Tk
Obtain the traversed path patht withmethod conditions {M Ci }Derive the pre-condition Ct ∧ Dk′ ∧ F S ′ for patht
with {M Ci } from the post-condition Dk ∧ F S
Validate the implication Tk ∧ Ct ⇒ Dk′ ∧ F S ′Figure 1. The framework of TBFV• The first step is to randomly generate a test caset satisfying some test condition Tk . Only one
test condition will be satisfied due to the wellformedness of the specification. Note that when
the program involves with a method invocation of
a complex component (such as Vector, ArrayList
and LinkedList in JAVA), the test case t needs tocontain the initial component state.
• The second step is to execute program P with test
case t and obtain a traversed program path patht ,which is a sequence of guard conditions, assignment statements and method invocations. Eachmethod has already been equipped with a Hoare
tripe which may contain multiple activated guard
conditions. The activated guard condition M Ci of
the i-th invoked method should also be recorded.
• As the test case t must contain the initial component state, correspondingly, the post-condition
should be not only the defining condition Dk , but
the conjunction of the defining condition and thefinal component state Dk ∧ F S (each component
has a final state representation F S). Assuming
such post-condition, we can backwards derive thepre-condition Ct ∧ Dk′ ∧ F S ′ of patht with method
conditions {M Ci } where Ct is the conjunction ofguard conditions in patht after replacing all intermediate variables with expressions of input variables and Dk′ ∧F S ′ is obtained by replacing all output variables with expressions of input variables inthe derivation process.

2. The Framwork of TBFVIn formal methods, the first step to implement an
operation is usually to write a formal specification todescribe its requirements. The assumption for TBFV
is that the operation specification
Wn S can be represented
as a functional scenario form i=1 (Ti ∧ Di ) where Ti iscalled a test condition and Di is called a defining condition. A test condition is a constraint only on the input
variables, while a defining condition contains at least
one output variable. The functional scenario Ti ∧ Di
describes a single specific functional behavior: when Ti
is true, the output of the operation is defined
Wn using Di .
Given an operation specification S = i=1 (Ti ∧ Di )with a program P , the TBFV method is proposed totackle the problem whether both input and output variables satisfy Di after P is executed if input variables
satisfy the corresponding Ti .
The framework of TBFV is illustrated in Figure 1
and explained as follows.

• The final step is to find whether Tk ∧ Ct implies
Dk′ ∧ F S ′ with the aid of theorem provers. If it isa tautology, patht with method conditions {M Ci }is correct with respect to the specification S; otherwise, there must be errors in patht .
If the path correctness is ensured, all test cases validating Tk ∧ Ct will satisfy the specification. Then, we

39

SEA

ソフトウェア・シンポジウム 2023 in 仙台

can choose a test case t validating Tk ∧ ¬Ct to continue
the above steps.
Example 1. Consider a jump function f whose domain is the set of integers Z and output is(
1 x≥0
y = f (x) =0 x<0

derived a fault localization approach. In TBFV-SE,
the correctness of each path is also converted into atheorem obtained during a dynamic symbolic execution, rather than the derivation by Hoare logic. The
framework of TBFV-SE is illustrated in Figure 2 andexplained as follows.
• Naturally, the first step is also to generate a test
case t, but there is no need to fix a test condition.
The initial component state should be included in
the test case if some component method is invoked.

Then, the corresponding FSF S is(x ∈ Z ∧ x ≥ 0 ∧ y = 1) ∨ (x ∈ Z ∧ x < 0 ∧ y = 0)

• After executing program P with test case t, a traversed program path can be obtained. Replacing
test case t with symbol values and applying symbolic execution for that path, all the output variables, path conditions and component states are
finally related to the symbol values. We use Ct
and statet to denote path-condition, the integration of all path conditions and a symbolic stateincluding all output variables and all component
states, respectively.

Consider the following program:int jump(int x){
int y = 0;
if (x >= 0)y = (x + 2)/(x + 1);
return y;}where variable x is the input and variable y is the output. If the given input is x = 1, the corresponding
testing condition is x ∈ Z ∧ x ≥ 0 and defining condition is y = 1. Then we can derive the pre-condition forthe corresponding path as follows• Although the test case t only validates a testing
condition, there may exist other test cases, validating different testing conditions, which resultin the same traversed path. If the implication
Ct ∧ Ti ⇒ statet ∧ Di is tautologous, it means thatthe test cases validating testing condition Ti andresulting in this traversed path satisfy the specification. There, the theorem we intend to prove is∀i Ct ∧ Ti ⇒ statet ∧ Di , which ensures the pathcorrectness.

{x ≥ 0 ∧ 1 = (x + 2)/(x + 1)}
y=0{x ≥ 0 ∧ 1 = (x + 2)/(x + 1)}
x >= 0{1 = (x + 2)/(x + 1)}
y = (x + 2)/(x + 1)
{y = 1}• Branch sequence coverage (BSC) is proposed toautomatically partition the domain by dynamically gathering all the necessary symbolic paths
since each symbolic path is selected to represent
a sub-domain. This partition is depended on a
dynamic light analysis of code structure without
judging if the branch conditions are serialized ornested. Unlike conventional partition testing selecting classical values from classes to test, BSC
focuses on automatically selecting a real symbolic
path for representing each sub-domain according
to the real structure of codes. There is an algorithm to automatically find test cases satisfying
BSC in [11].

The next step is to consider the implicationx ∈ Z ∧ x ≥ 0 ∧ x ≥ 0 ⇒ 1 = (x + 2)/(x + 1)
which is true for x > 0 due to the division operationof integers but false when x = 0. If we only use testing, we may select many test cases in which x ̸= 0
and produce the test results as expected. In this case,the contradiction can not be revealed. However, using
TBFV, we can get the same path and implication oncea test case x ≥ 0 is chosen, and find the contradiction.

3. The Framework of TBFV-SE• A fault localization algorithm is proposed in [12]to provide a rigorous way to automatically analyze
the correctness of statements in a program basedon the theorems of the traversed paths and help
locate the faults in a small set of statements byexamining very small percentage of the code.

Testing-based formal verification with symbolic execution (TBFV-SE) has already been a method to automatically verify the correctness of all the representative program paths given the formal specifications and

40

SEA

ソフトウェア・シンポジウム 2023 in 仙台

Generate a test case t
Carry out the symbolic execution of the program
path traversed by t to obtain a symbolic
path-condition Ct and a symbolic state statet
Validate the theorem ∀i Ct ∧ Ti ⇒ statet ∧ Di
Continue generating test cases until
they satisfy branch sequence coverage criterion
Analyze the fault location
if there are incorrect theorems
Figure 2. The framework of TBFV-SE
Example 2. Reconsidering Example 1 with TBFV-SE,
the derivation of path-condition and the record of states
for the traversed path by the input x with numeric value
1 and symbolic value X is displayed in Table 1. The
last line of second column of Table 1 shows both thesymbolic state and symbolic path-condition. Then, theinduced theorem istheorems. Further, TBFV-SE has been enriched with
two algorithms to find representative program paths
and analyze the correctness of statements. We mainlycompare the common procedures of TBFV and TBFVSE.
Given a test case t, TBFV and TBFV-SE will obtain the same program path patht . The difference isthe way to derive the theorems, as depicted in Example 1 and 2. In TBFV, we need to preselect a functional
scenario Ti ∧ Di and the derived theorem can only represent whether the traversed path satisfies that functional scenario. In TBFV-SE, the derived theorem canbe used to judge whether the traversed path satisfies
all functional scenarios. Given the test cases inducing a
traversed path, if some of them validate a testing condition Ti and the rest validate another testing condition
Tj , we just need one derivation process of the theorem
in TBFV-SE while we should need two derivation processes of the theorem in TBFV. In that case, TBFVSE should be more efficient than TBFV. Nevertheless,
TBFV will have an advantage than TBFV-SE in cases
including many intermediate variables and irrelevant
variables, as depicted in Example 3.
Example 3. Consider the following program which
implements a piecewise function,

X+2
)∧
X+1
X+2
)
(x ∈ Z ∧ x < 0 ∧ x ≥ 0 ⇒ y = 0 ∧ y =X+1(x ∈ Z ∧ x ≥ 0 ∧ x ≥ 0 ⇒ y = 1 ∧ y =int piece(float x){
float y1 = 1 − x;
float y2 = 2x;
float y3 = 1/x;
if (x < −4)y = y1;else if (−4 ≤ x ≤ 0)y = y2;else
y = y3;return y;}where the first sub-formula is false while the second subformula is true. We just use this simple example toshow how symbolic execution help derive theorems in
TBFV-SE.
Table 1. Single path of symbolic execution
program code
symbolic execution
input: x = 1
int jump(int x)
symbolic value of x : X
int y = 0state: {y = 0}
if (x >= 0)
path-condition: X ≥ 0
y = (x + 2)/(x + 1)
state: {y = X+2
X+1 }
X+2
return y{y = X+1}, X ≥ 0

4. Merits and Demerits

For any input value, the traversed path must include thefirst three assignment statements. Assume the input is
0 and the corresponding functional scenario is T ∧ D
where D only includes the variable y, the derivation by
Hoare logic is below.
{ − 4 ≤ x ≤ 0 ∧ D(2x/y)}y1 = 1 − x{ − 4 ≤ x ≤ 0 ∧ D(2x/y)}y2 = 2x{ − 4 ≤ x ≤ 0 ∧ D(y2/y)}

As for our goal to verify whether a program satisfies its corresponding specification, TBFV and TBFVSE can both automatically generate test cases, obtain
traversed paths and induce theorems. Next, external
theorem provers will be used to validate the induced

41

SEA

ソフトウェア・シンポジウム 2023 in 仙台

y3 = 1/x{ − 4 ≤ x ≤ 0 ∧ D(y2/y)}−4 ≤ x ≤ 0{D(y2/y)}y = y2{D}
Then, the theorem to be proved in TBFV is

5. Conclusion and Future WorkTBFV and TBFV-SE are both currently able to reduce test cost by ensuring path correctness, while eachof them has its advantages and disadvantages. TBFVSE includes a fault localization algorithm based on thetraversed paths obtained by test cases satisfying branchsequence coverage criterion. In the future, we intend
to locate faults in a single path which is proved to haveerrors by TBFV.

T ∧ −4 ≤ x ≤ 0 ⇒ D(2x/y)
The corresponding symbolic execution is shown in Table
2 where we omit the skipped statements. Then, thetheorem to be proved in TBFV-SE is

References[1] Peled, D. A. “Software Reliability Methods”,
Springer, 2001.

T ∧ X ≥ 4 ∧ −4 ≤ X ≤ 0⇒D ∧ y1 = 1 − X ∧ y2 = 2X ∧ y3 =1
∧ y = 2X
X

Table 2. Symbolic execution for x = 0
program code
symbolic execution
input: x = 0
int piece(float x)
symbolic value of x : X
float y1 = 1 − xstate:{y1 = 1 − X}float y2 = 2x
state:{y1 = 1 − X, y2 = 2X}
state:{y1 = 1 − X, y2 = 2X,
float y3 = 1/xy3 = 1X }if x < −4path-condition X ≥ 4
path-condition X ≥ 4∧
else if −4 ≤ x ≤ 0−4 ≤ X ≤ 0state:{y1 = 1 − X, y2 = 2X,y = y2y3 = 1X , y = 2X}{y1 = 1 − X, y2 = 2X,
y3 = 1X , y = 2X},
return y
X ≥ 4 ∧ −4 ≤ X ≤ 0
Obviously, the theorem obtained by TBFV-SE is
more complex than the theorem obtained by TBFV,
Actually, we must simplify the theorem obtained by
TBFV-SE as[2] Hoare, C. A. R. and Wirth, N. “An Axiomatic Definition of the Programming Language PASCAL”,
Acta Informatica 2, pp. 335-355, 1973.
[3] Cadar, C. and Sen, K. “Symbolic Execution for
Software Testing: Three Decades Later”, ACM,
2013.
[4] Whittaker, J. A. “What is software testing? Why is
it so hard? Practice Tutorial”, IEEE Softw. 17(1),pp. 70-79, 2000.
[5] Chen, Y. and Liu, S. “An Approach to Detecting
Domain Errors Using Formal Specification-Based
Testing”, Proceedings of APSEC 2004: 276-283.
[6] Liu, S. “Utilizing Hoare Logic to Strengthen Testing for Error Detection in Program”,Proceedings ofTuring-100 2012, pp. 229-238.
[7] Liu, S. and Nakajima, S. “Combining SpecificationBased Testing, Correctness Proof, and Inspection
for Program Verification in Practice”, Proceedingsof SOFL+MSVL 2013, pp. 3-16.
[8] Liu, S. “A Tool Supported Testing Method for Reducing Cost and Improving Quality”, Proceedingsof QRS 2016, pp. 448-455.

T ∧ X ≥ 4 ∧ −4 ≤ X ≤ 0 ⇒ D ∧ y = 2X
which can be proved by theorem provers, since the formulas y1 = 1 − X, y2 = 2X and y3 = 1X are undecidable
equations. Moreover, D ∧ y = 2X can be further simplified as D(2X/y). Therefore, the theorem obtained by
TBFV is more concise and there is no need to record intermediate variables (e.g. y2) and irrelevant variables(e.g. y1 and y3) in TBFV.

[9] Liu, A. and Liu, S. “Enhancing the Capability ofTesting-Based Formal Verification by Handling Operations in Software Packages”, IEEE Trans. Software Eng. 49(1), pp. 304-324, 2023.
[10] Wang, R. and Liu, S. “TBFV-SE: Testing-Based
Formal Verification with Symbolic Execution”,
Proceedings of QRS 2018, pp. 59-66.

42

SEA

ソフトウェア・シンポジウム 2023 in 仙台[11] Wang, R. and Liu, S. “Branch Sequence Coverage Criterion for Testing-Based Formal Verification
with Symbolic Execution”, Proceedings of QRS-C
2019, pp. 205-212.
[12] Wang, R. et al. “A Fault Localization Approach
Derived from Testing-Based Formal Verification”,
Proceedings of ICECCS 2022, pp. 165-170.
[13] Liu, H. et al. “Verifying and Improving Neural Networks Using Testing-Based Formal Verification”, Proceedings of SOFL+MSVL 2022, pp. 126141.

43

SEA