Conflict-Directed Graph Coverage
2015 (English)In: NASA FORMAL METHODS (NFM 2015), 2015, 327-342 p.Conference paper (Refereed)
Many formal method tools for increasing software reliability apply Satisfiability Modulo Theories (SMT) solvers to enumerate feasible paths in a program subject to certain coverage criteria. Examples include inconsistent code detection tools and concolic test case generators. These tools have in common that they typically treat the SMT solver as a black box, relying on its ability to efficiently search through large search spaces. However, in practice the performance of SMT solvers often degrades significantly if the search involves reasoning about complex control-flow. In this paper, we open the black box and devise a new algorithm for this problem domain that we call conflict-directed graph coverage. Our algorithm relies on two core components of an SMT solver, namely conflict-directed learning and deduction by propagation, and applies domain-specific modifications for reasoning about control-flow graphs. We implemented conflict-directed coverage and used it for detecting code inconsistencies in several large Java open-source projects with over one million lines of code in total. The new algorithm yields significant performance gains on average compared to previous algorithms and reduces the running times on hard search instances from hours to seconds.
Place, publisher, year, edition, pages
2015. 327-342 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9058
Computer and Information Science
IdentifiersURN: urn:nbn:se:uu:diva-266294DOI: 10.1007/978-3-319-17524-9_23ISI: 000361977000023ISBN: 978-3-319-17524-9ISBN: 978-3-319-17523-2OAI: oai:DiVA.org:uu-266294DiVA: diva2:867754
7th NASA Formal Methods Symposium (NFM), APR 27-29, 2015, Pasadena, CA