Test Case Generation and Dynamic Mixed-Integer Linear Arithmetic Constraint Solving
Abstract
Manually generating test cases for unit tests is a tedious task, especially when highcode coverage is desired. We developed the tool Muggl, which generates test cases basedon symbolic execution and constraint solving. The solution of constraints for this purposeis by no means a trivial task and greatly attributes to the total runtime. Therefore, we developed a solver for linear constraints adapted to the special needs of Muggl. It takes into account the particularities of constraint retrieval through symbolic execution. Specificallyt, it is capable of incremental addition and backtracking of constraints. Our paper introduces the topic and gives an overview of related work. Based on the problems discovered in other solvers, the distinctive features of our dynamic mixed-integer linear arithmetic (MILA) are introduced. We focus on adding and removing constraints and handling rounding errors that occur when test cases are generated. The evaluation results demonstrate the feasibility of our approach.
Keywords
test-case generation; Java; symbolic execution; constraint solving; simplex algorithm