Online Archive of University of Virginia Scholarship
Finding and Fixing Bugs in Liquid Haskell1201 views
Author
Tondwalkar, Anish, Computer Science - School of Engineering and Applied Science, University of Virginia
Advisors
Weimer, Westley, Department of Computer Science, University of Virginia
Abstract
Dependent types provide strong guarantees but can be hard to program, admitting mistakes in the implementation as well as the specification. We present algorithms for resolving verification failures by both finding bugs in implementations and also completing annotations in the Liquid Haskell refinement type framework. We present a fault localization algorithm for finding likely bug locations when verification failure stems from a bug in the implementation. We use the type checker as an oracle to search for a set of minimal unsatisfiable type constraints that map to possible bug locations. Conversely, we present an algorithm based on Craig interpolation to discover predicates that allow the type checker to verify programs that would otherwise be deemed unsafe due to inadequate type annotations. We evaluate our algorithms on an indicative benchmark of Haskell programs with Liquid Haskell type annotations. Our fault localization algorithm localizes more bugs than the vanilla Liquid Haskell type checker while still returning a small number of false positives. Our predicate discovery algorithm infers refinements types for large classes of benchmark programs, including all those that admit bounded constraint unrolling. In addition, the design of our algorithms allows them to be effectively extended to other typing systems.
Degree
MS (Master of Science)
Keywords
Verification; Type Systems; Programming Languages
Language
English
Rights
All rights reserved (no additional license for public reuse)
Tondwalkar, Anish. Finding and Fixing Bugs in Liquid Haskell. University of Virginia, Computer Science - School of Engineering and Applied Science, MS (Master of Science), 2016-04-19, https://doi.org/10.18130/V3V685.