ABSTRACT. Dynamic symbolic execution is a technique that analyses programs by gathering mathematical constraints along execution paths. To achieve bit-level precision, one must use the theory of bitvectors. However, other theories might achieve significantly higher performance, justifying in some cases the possible loss of precision.

In this paper, we explore the impact of using the theory of integers on the precision and performance of dynamic symbolic execution of C programs. In particular, we compare an implementation of the symbolic executor KLEE using a partial solver based on the theory of integers, with a standard implementation of KLEE using a solver based on the theory of bitvectors. To our surprise, our evaluation on the ECA set of Test-Comp benchmarks and GNU Coreutils revealed that for most applications the integer solver did not lead to any loss of precision, but the overall performance difference was not significant.

ABSTRACT. Software testing is a time consuming and error prone activity, mostly manual in most industries. One approach to increase productivity is to automatically generate tests. In this paper, we focus on automatic generation of structural unit tests of safety-critical embedded software. Our purpose is to make a tool that integrates seamlessly with existing test processes in industry. We use genetic algorithms and automatic stub generation to quickly and automatically produce all test cases of a software satisfying a given coverage criteria, using only the software under test as input. Moreover, we combine those genetic algorithms with formal methods to determine unfeasible test objectives and help on the coverage of difficult test objectives. We implemented our approach in a tool and tested it on two real-world industrial projects, demonstrating that our approach can reliably generate test cases when feasible or demonstrate they are infeasible for 99% of the MCDC test objectives in about half an hour for 80k source lines.

ABSTRACT. We provide a model-based testing approach for systems comprising both state-transition based control flow, and data elements such as variables and data-dependent transitions. We propose test generation and execution, based on model-coverage: we generate test cases that reach all transitions of the model. To obtain a test case reaching a certain transition, we need to combine reachability in the control flow, and satisfiability of the data elements of the model. Concrete values for data parameters are generated on-the-fly, i.e., during test execution, such that received outputs from the system can be taken into account for the inputs later provided in test execution. Due to undecidability of the satisfiability problem, SMT solvers may return result `unknown'. Our algorithm deals with this explicitly. We implemented our method in Maude combined with Z3, and use this to demonstrate the applicability of our method on the Bounded Retransmission Protocol benchmark. As a result, we find that we need 8 times less inputs and outputs to discover bugs in mutants, i.e., in non-conforming variants of the specification, than when using random testing as implemented by the tool TorXakis.