LCTD

Recently there has been much interest in combining underapproximation and overapproximation based approaches to software verification. Such a technique is employed by the DASH algorithm originally developed at Microsoft, which generates tests to gradually improve the accuracy of an underapproximation of the program under test. Simultaneously, an overapproximating abstraction of the program is refined with information gathered from the test generation. We present LCTD, an open source tool that implements the DASH algorithm for the verification of C programs compiled on the LLVM compiler framework. Our implementation is an extension of the dynamic symbolic execution tool LCT. We also present a detailed description of our method for constructing the weakest precondition based refinement operator employed by DASH for instructions of the LLVM internal representation. Our construction handles pointers and array indexing. To maintain a mapping between concrete executions and the abstraction DASH needs to evaluate predicates on the concrete states visited during test executions. A straightforward implementation might store the complete concrete states of each executed test or might employ expensive re-executions to recover the concrete states. We present a technique which allows only the concrete values of pointer variables to be stored while still requiring no re-executions. Finally we present a case study to show the viability of our tool. We also document a more powerful abstraction refinement method for DASH that exploits unsatisfiable regions and evaluate its effect.