Finding Bugs in Functional Programs using Theorem Provers

Abstract

This thesis investigates whether automated first-order theorem provers can be efficiently used to discover bugs in Haskell programs by extracting counterexamples to incorrect program properties. To enable counterexample extraction, we present an alternative translation from Haskell programs to first-order logic that reformulates programs to purely equational first-order theories and properties to existential conjectures. The translation to the proposed encoding builds on the pre-existing Haskell → TIP → TPTP translation pipeline by introducing a sequence of transformations that preserve the semantics of the original program with the goal of making the resulting theories better suited for equational theorem provers. The approach is evaluated using the theorem provers Twee, E and Vampire on a collection of Haskell benchmarks. The results show that provers are capable of successfully extracting counterexamples to incorrect Haskell properties, and that the proposed encoding does in fact improve their performance compared with the one produced by the pre-existing translation. Among the evaluated provers, Twee consistently produced the strongest results on the proposed encoding, while E achieved the best overall performance when combined with an appropriate lexicographic path ordering that approximates goal-directed proof search. The evaluation identifies weak goal direction as the principal practical limitation of theorem-prover counterexample extraction and the resulting time inefficiency, as its main disadvantage in comparison to property-based testing. However, our work also demonstrates that theorem-prover counterexample extraction offers capabilities which property-based testing doesn’t, including the successful extraction of counterexamples to higher-order properties, ultimately making it a promising direction for future research on automated bug finding in functional programs.