uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Conflict-Directed Graph Coverage
NYU, New York, NY USA..
SRI Int, Menlo Pk, CA 94025 USA..
SRI Int, Menlo Pk, CA 94025 USA..
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Show others and affiliations
2015 (English)In: NASA FORMAL METHODS (NFM 2015), 2015, 327-342 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9058
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:uu:diva-266294DOI: 10.1007/978-3-319-17524-9_23ISI: 000361977000023ISBN: 978-3-319-17524-9 (print)ISBN: 978-3-319-17523-2 (print)OAI: oai:DiVA.org:uu-266294DiVA: diva2:867754
Conference
7th NASA Formal Methods Symposium (NFM), APR 27-29, 2015, Pasadena, CA
Available from: 2015-11-06 Created: 2015-11-06 Last updated: 2017-01-19Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Rümmer, Philipp

Search in DiVA

By author/editor
Rümmer, Philipp
By organisation
Computer Systems
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 311 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf