The IntiSa Approach: Test Input Data Generation for Non-primitive Data Types by Means of SMT Solver Based Bounded Model Checking

2011 ◽  
Author(s):  
Stefan J. Galler ◽  
Thomas Quaritsch ◽  
Martin Weiglhofer ◽  
Franz Wotawa
Keyword(s):  
Model Checking ◽  
Input Data ◽  
Bounded Model Checking ◽  
Data Generation ◽  
Data Types ◽  
Smt Solver ◽  
Test Input

scholarly journals Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds

2021 ◽  
pp. 218-239
Author(s):  
Pablo Ponzio ◽  
Ariel Godio ◽  
Nicolás Rosner ◽  
Marcelo Arroyo ◽  
Nazareno Aguirre ◽  
...  
Keyword(s):  
Model Checking ◽  
Data Structures ◽  
Efficient Algorithm ◽  
Bounded Model Checking ◽  
Model Checker ◽  
Data Types ◽  
Dynamic Data Structures ◽  
Dynamic Data ◽  
Software Model ◽  
Improve Model

AbstractSoftware model checkers are able to exhaustively explore different bounded program executions arising from various sources of non-determinism. These tools provide statements to produce non-deterministic values for certain variables, thus forcing the corresponding model checker to consider all possible values for these during verification. While these statements offer an effective way of verifying programs handling basic data types and simple structured types, they are inappropriate as a mechanism for nondeterministic generation of pointers, favoring the use of insertion routines to produce dynamic data structures when verifying, via model checking, programs handling such data types.We present a technique to improve model checking of programs handling heap-allocated data types, by taming the explosion of candidate structures that can be built when non-deterministically initializing heap object fields. The technique exploits precomputed relational bounds, that disregard values deemed invalid by the structure’s type invariant, thus reducing the state space to be explored by the model checker. Precomputing the relational bounds is a challenging costly task too, for which we also present an efficient algorithm, based on incremental SAT solving.We implement our approach on top of the bounded model checker, and show that, for a number of data structures implementations, we can handle significantly larger input structures and detect faults that is unable to detect.

scholarly journals Test Input Data Generation for Choiceless Program Nets

2020 ◽  
Vol 14 (1) ◽  
pp. 37-45
Author(s):  
Wu Biao ◽  
Qi-Wei Ge
Keyword(s):  
Computational Complexity ◽  
Software Testing ◽  
Input Data ◽  
Satisfiability Modulo Theories ◽  
Divide And Conquer ◽  
Polynomial Algorithms ◽  
Software System ◽  
Data Generation ◽  
Test Input ◽  
Large Software

Software testing is an important problem in designing a large software system and this problem is difficult to be solved due to its computational complexity. We try to use program nets to approach this problem and have proposed algorithms to divide a whole program net into subnets that can structurally cover the original one based on divide-and-conquer method. This paper aims to solve the remaining task of our approach, that is how to find test input data for each subnet to be called choiceless program net. Firstly, definitions of program nets are extended and the properties of choiceless program nets are analysed. Secondly, polynomial algorithms are proposed to get all constraint conditions of any given choiceless program nets. Finally, a method to generate test input data under the obtained constraint conditions is proposed by adopting an SMT (Satisfiability Modulo Theories) solver, $Z3$ prover, and also an example is given to show the usefulness of our method.

Detecting buffer overflow via automatic test input data generation

2008 ◽  
Vol 35 (10) ◽  
pp. 3125-3143 ◽  
Author(s):  
C. Del Grosso ◽  
G. Antoniol ◽  
E. Merlo ◽  
P. Galinier
Keyword(s):  
Input Data ◽  
Buffer Overflow ◽  
Data Generation ◽  
Automatic Test ◽  
Test Input

Bounded Model Checking for Probabilistic Computation Tree Logic

2012 ◽  
Vol 23 (7) ◽  
pp. 1656-1668 ◽  
Author(s):  
Cong-Hua ZHOU ◽  
Zhi-Feng LIU ◽  
Chang-Da WANG
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree
Sign in / Sign up

Export Citation Format

Share Document