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 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.