  In this paper, we study the problem of generating inputs to a higher-order
program causing it to error. We first study the problem in the setting of PCF,
a typed, core functional language and contribute the first relatively complete
method for constructing counterexamples for PCF programs. The method is
relatively complete in the sense of Hoare logic; completeness is reduced to the
completeness of a first-order solver over the base types of PCF. In practice,
this means an SMT solver can be used for the effective, automated generation of
higher-order counterexamples for a large class of programs.
  We achieve this result by employing a novel form of symbolic execution for
higher-order programs. The remarkable aspect of this symbolic execution is that
even though symbolic higher-order inputs and values are considered, the path
condition remains a first-order formula. Our handling of symbolic function
application enables the reconstruction of higher-order counterexamples from
this first-order formula.
  After establishing our main theoretical results, we sketch how to apply the
approach to untyped, higher-order, stateful languages with first-class
contracts and show how counterexample generation can be used to detect contract
violations in this setting. To validate our approach, we implement a tool
generating counterexamples for erroneous modules written in Racket.
