Conflict-directed graph coverage

Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanović, Philipp Rümmer, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings
EditorsKlaus Havelund, Gerard Holzmann, Rajeev Joshi
PublisherSpringer Verlag
Pages327-342
Number of pages16
ISBN (Print)9783319175232
DOIs
StatePublished - 2015
Event7th International Symposium on NASA Formal Methods, NFM 2015 - Pasadena, United States
Duration: Apr 27 2015Apr 29 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9058
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th International Symposium on NASA Formal Methods, NFM 2015
CountryUnited States
CityPasadena
Period4/27/154/29/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Conflict-directed graph coverage'. Together they form a unique fingerprint.

  • Cite this

    Schwartz-Narbonne, D., Schäf, M., Jovanović, D., Rümmer, P., & Wies, T. (2015). Conflict-directed graph coverage. In K. Havelund, G. Holzmann, & R. Joshi (Eds.), NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings (pp. 327-342). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9058). Springer Verlag. https://doi.org/10.1007/978-3-319-17524-9_23