Solving complex path conditions through heuristic search on induced polytopes

Peter Dinges, Gul A Agha

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

Abstract

Test input generators using symbolic and concolic execution must solve path conditions to systematically explore a program and generate high coverage tests. However, path conditions may contain complicated arithmetic constraints that are infeasible to solve: a solver may be unavailable, solving may be computationally intractable, or the constraints may be undecidable. Existing test generators either simplify such constraints with concrete values to make them decidable, or rely on strong but incomplete constraint solvers. Unfortunately, simplification yields coarse approximations whose solutions rarely satisfy the original constraint. Moreover, constraint solvers cannot handle calls to native library methods. We show how a simple combination of linear constraint solving and heuristic search can overcome these limitations. We call this technique Concolic Walk. On a corpus of 11 programs, an instance of our Concolic Walk algorithm using tabu search generates tests with two- to three-times higher coverage than simplification-based tools while being up to five-times as efficient. Furthermore, our algorithm improves the coverage of two state-of-the-art test generators by 21% and 32%. Other concolic and symbolic testing tools could integrate our algorithm to solve complex path conditions without having to sacrifice any of their own capabilities, leading to higher overall coverage.

Original languageEnglish (US)
Title of host publication22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014 - Proceedings
PublisherAssociation for Computing Machinery
Pages425-436
Number of pages12
ISBN (Electronic)9781450330565
DOIs
StatePublished - Nov 16 2014
Event22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014 - Hong Kong, China
Duration: Nov 16 2014Nov 21 2014

Publication series

NameProceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering
Volume16-21-November-2014

Other

Other22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014
CountryChina
CityHong Kong
Period11/16/1411/21/14

Keywords

  • Concolic testing
  • Local search
  • Non-linear constraints

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Solving complex path conditions through heuristic search on induced polytopes'. Together they form a unique fingerprint.

  • Cite this

    Dinges, P., & Agha, G. A. (2014). Solving complex path conditions through heuristic search on induced polytopes. In 22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014 - Proceedings (pp. 425-436). (Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering; Vol. 16-21-November-2014). Association for Computing Machinery. https://doi.org/10.1145/2635868.2635889