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

Direct link
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 (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.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9058
National Category
Computer and Information Science
URN: 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
Available from: 2015-11-06 Created: 2015-11-06 Last updated: 2015-11-06Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 134 hits
ReferencesLink to record
Permanent link

Direct link