Item Details

Print View

Finding and Fixing Bugs in Liquid Haskell

Tondwalkar, Anish
Format
Thesis/Dissertation; Online
Author
Tondwalkar, Anish
Advisor
Weimer, Westley
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.
Language
English
Published
University of Virginia, Department of Computer Science, MS, 2016
Published Date
2016-04-19
Degree
MS
Collection
Libra ETD Repository
In CopyrightIn Copyright
▾See more
▴See less

Availability

Read Online