swMATH ID: 17728
Software Authors: Saarikivi, Olli; Heljanko, Keijo
Description: LCTD: test-guided proofs for C programs on LLVM. Recently there has been much interest in combining underapproximation and overapproximation based approaches to software verification. Such a technique is employed by the {sc 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.par We present LCTD, an open source tool that implements the {sc 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 {sc Dash} for instructions of the LLVM internal representation. Our construction handles pointers and array indexing.par To maintain a mapping between concrete executions and the abstraction {sc 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.par Finally we present a case study to show the viability of our tool. We also document a more powerful abstraction refinement method for {sc Dash} that exploits unsatisfiable regions and evaluate its effect.
Homepage: http://www.sciencedirect.com/science/article/pii/S2352220815001157
Keywords: automated testing; verification; dynamic symbolic execution; abstraction refinement; predicate abstraction; weakest precondition
Related Software: STP; LCT; jCUTE; SMACK; BoogiePL; Vellvm; YOGI; Threader; CBMC; CPAchecker; Predator; DART; KLEE; LLVM; z3; CUTE; Boolector
Cited in: 1 Publication

Citations by Year