Sound and Complete Concolic Testing for Higher-order Functions

Shu Hung You*, Robert Findler, Christos Dimoulas

*Corresponding author for this work

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

Abstract

Higher-order functions have become a staple of modern programming languages. However, such values stymie concolic testers, as the SMT solvers at their hearts are inherently first-order. This paper lays a formal foundations for concolic testing higher-order functional programs. Three ideas enable our results: (i) our tester considers only program inputs in a canonical form; (ii) it collects novel constraints from the evaluation of the canonical inputs to search the space of inputs with partial help from an SMT solver and (iii) it collects constraints from canonical inputs even when they are arguments to concretized calls. We prove that (i) concolic evaluation is sound with respect to concrete evaluation; (ii) modulo concretization and SMT solver incompleteness, the search for a counter-example succeeds if a user program has a bug and (iii) this search amounts to directed evolution of inputs targeting hard-to-reach corners of the program.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings
EditorsNobuko Yoshida
PublisherSpringer Science and Business Media Deutschland GmbH
Pages635-663
Number of pages29
ISBN (Print)9783030720186
DOIs
StatePublished - 2021
Event30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021 - Luxembourg, Luxembourg
Duration: Mar 27 2021Apr 1 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12648 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021
Country/TerritoryLuxembourg
CityLuxembourg
Period3/27/214/1/21

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Sound and Complete Concolic Testing for Higher-order Functions'. Together they form a unique fingerprint.

Cite this