  Symbolic execution is a program analysis technique executing programs with
symbolic instead of concrete inputs. This principle allows for exploring many
program paths at once. Despite its wide adoption -- in particular for program
testing -- little effort was dedicated to studying the semantic foundations of
symbolic execution. Without these foundations, critical questions regarding the
correctness of symbolic executors cannot be satisfyingly answered: Can a
reported bug be reproduced, or is it a false positive (soundness)? Can we be
sure to find all bugs if we let the testing tool run long enough
(completeness)? This paper presents a systematic approach for engineering
provably sound and complete symbolic execution-based bug finders by relating a
programming language's operational semantics with a symbolic semantics. In
contrast to prior work on symbolic execution semantics, we address the
correctness of critical implementation details of symbolic bug finders,
including the search strategy and the role of constraint solvers to prune the
search space. We showcase our approach by implementing WiSE, a prototype of a
verified bug finder for an imperative language, in the Coq proof assistant and
proving it sound and complete. We demonstrate that the design principles of
WiSE survive outside the ecosystem of interactive proof assistants by (1)
automatically extracting an OCaml implementation and (2) transforming WiSE to
PyWiSE, a functionally equivalent Python version.
