Lazy Symbolic Execution, Counterfactual Examples and Haskell Constraint Solving

G2 is a symbolic execution engine for non-strict functional languages, such as Haskell. Although symbolic execution has been widely applied to languages with strict semantics, symbolic execution for lazily evaluated languages is less explored. In this talk, I will describe the design of the engine, and the lazy reduction rules it uses to reduce expressions to a normal form.

In addition to presenting the design of G2, I will describe how we have applied G2 to two different use cases. First, I will present counterfactual symbolic execution, a new technique to debug modular verification errors. Using counterfactual symbolic execution, users can diagnose verification errors that arise due to weak specifications, rather than bugs in their code. To demonstrate the effectiveness of the technique, I will present an evaluation on a collection of verification errors, gathered from students learning to use LiquidHaskell. As a second use case, I will describe a library, G2Q, that allows constraints to be written as Haskell predicates, and solved during the runtime of a Haskell program. As opposed to directly calling an SMT solver or using an SMT solver’s API, G2Q predicates are significantly shorter, and allow reusing datatypes and functions defined in Haskell libraries. In addition to presenting the design of the library, I will show several examples of how it can be used.

Bill Hallahan is a graduate student of Computer Student at Yale University, advised by Ruzica Piskac. Recently, his research has focused on techniques for symbolic execution and program synthesis. In the past, he has worked on applying formal methods to computer networks, including the development of techniques to automatically repair firewalls, and to verify P4 programs.