Building a Symbolic Execution Engine for Haskell

Symbolic execution is a powerful software analysis technique that reasons about the possible execution states of a program due to logical branching. Historically, such techniques are primarily geared towards imperative languages such as C and Java, with less effort in the development of frameworks for functional languages. While such works do exist, many are focused on contract-based analysis, and some lack full support for reasoning about functional expressions. In this paper we outline the application of symbolic execution techniques to Haskell. Our methods for program model extraction, defunctionalization, execution semantics, and constraint solving have strong implications for static analysis based testing, and for future work in program verification and synthesis. CCS Concepts ˆ Software and its engineering Functional languages;