Concolic Testing Heap-Manipulating Programs

Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun

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

    88 Downloads (Pure)

    Abstract

    Concolic testing is a test generation technique which works effectively
    by integrating random testing generation and symbolic execution. Existing concolic
    testing engines focus on numeric programs. Heap-manipulating programs
    make extensive use of complex heap objects like trees and lists. Testing such
    programs is challenging due to multiple reasons. Firstly, test inputs for such programs
    are required to satisfy non-trivial constraints which must be specified precisely.
    Secondly, precisely encoding and solving path conditions in such programs
    are challenging and often expensive. In this work, we propose the first
    concolic testing engine called CSF for heap-manipulating programs based on separation logic. CSF effectively combines specification-based testing and concolic execution for test input generation. It is evaluated on a set of challenging heap-manipulating programs. The results show that CSF generates valid test inputs with high coverage efficiently. Furthermore, we show that CSF can be potentially used in combination with precondition inference tools to reduce the user effort.
    Original languageEnglish
    Title of host publication23rd International Symposium on Formal Methods (FM 2019)
    PublisherSpringer
    Number of pages21
    Publication statusAccepted/In press - 12 Jun 2019
    Event23rd International Symposium on Formal Methods - Porto, Portugal
    Duration: 9 Oct 201911 Oct 2019
    https://www.youtube.com/channel/UC5rZj0AyBudca0YRgEAX-Ow/

    Conference

    Conference23rd International Symposium on Formal Methods
    Abbreviated titleFM2019
    CountryPortugal
    CityPorto
    Period9/10/1911/10/19
    Internet address

    Fingerprint Dive into the research topics of 'Concolic Testing Heap-Manipulating Programs'. Together they form a unique fingerprint.

  • Cite this

    Pham, L. H., Le, Q. L., Phan, Q-S., & Sun, J. (Accepted/In press). Concolic Testing Heap-Manipulating Programs. In 23rd International Symposium on Formal Methods (FM 2019) Springer.