LCTD

Olli Saarikivi, Keijo Heljanko

Research output: Contribution to journalArticleScientificpeer-review

Abstract

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.
Original languageEnglish
JournalJournal of Logical and Algebraic Methods in Programming
Volume85
Issue number6
Pages (from-to)1292-1317
ISSN2352-2208
DOIs
Publication statusPublished - 2016
Externally publishedYes
MoE publication typeA1 Journal article-refereed

Fields of Science

  • Abstraction refinement
  • Automated testing
  • Dynamic symbolic execution
  • Predicate abstraction
  • Verification
  • Weakest precondition

Cite this