LCTD: Test-guided proofs for C programs on LLVM

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.