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
PublisherSpringer Verlag
Pages327-342
Number of pages16
Volume9058
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Directed graphs
Directed Graph
Modulo
Coverage
Black Box
Reasoning
Flow graphs
Software Reliability
Software reliability
Flow Graphs
Formal methods
Formal Methods
Deduction
Flow Control
Flow control
Inconsistency
Inconsistent
Open Source
Search Space
Java

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Schwartz-Narbonne, D., Schäf, M., Jovanović, D., Rümmer, P., & Wies, T. (2015). Conflict-directed graph coverage. In NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings (Vol. 9058, 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

Conflict-directed graph coverage. / Schwartz-Narbonne, Daniel; Schäf, Martin; Jovanović, Dejan; Rümmer, Philipp; Wies, Thomas.

NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. Vol. 9058 Springer Verlag, 2015. p. 327-342 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9058).

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

Schwartz-Narbonne, D, Schäf, M, Jovanović, D, Rümmer, P & Wies, T 2015, Conflict-directed graph coverage. in NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. vol. 9058, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9058, Springer Verlag, pp. 327-342, 7th International Symposium on NASA Formal Methods, NFM 2015, Pasadena, United States, 4/27/15. https://doi.org/10.1007/978-3-319-17524-9_23
Schwartz-Narbonne D, Schäf M, Jovanović D, Rümmer P, Wies T. Conflict-directed graph coverage. In NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. Vol. 9058. Springer Verlag. 2015. p. 327-342. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-17524-9_23
Schwartz-Narbonne, Daniel ; Schäf, Martin ; Jovanović, Dejan ; Rümmer, Philipp ; Wies, Thomas. / Conflict-directed graph coverage. NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. Vol. 9058 Springer Verlag, 2015. pp. 327-342 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{635dabbcac784a97b1f5caf93872d16a,
title = "Conflict-directed graph coverage",
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.",
author = "Daniel Schwartz-Narbonne and Martin Sch{\"a}f and Dejan Jovanović and Philipp R{\"u}mmer and Thomas Wies",
year = "2015",
doi = "10.1007/978-3-319-17524-9_23",
language = "English (US)",
isbn = "9783319175232",
volume = "9058",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "327--342",
booktitle = "NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings",

}

TY - GEN

T1 - Conflict-directed graph coverage

AU - Schwartz-Narbonne, Daniel

AU - Schäf, Martin

AU - Jovanović, Dejan

AU - Rümmer, Philipp

AU - Wies, Thomas

PY - 2015

Y1 - 2015

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

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

UR - http://www.scopus.com/inward/record.url?scp=84942588923&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84942588923&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-17524-9_23

DO - 10.1007/978-3-319-17524-9_23

M3 - Conference contribution

SN - 9783319175232

VL - 9058

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 327

EP - 342

BT - NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings

PB - Springer Verlag

ER -