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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)